equal
deleted
inserted
replaced
115 map (perm_eq_constr dt_descr sorts perm_fn_frees i) constrs; |
115 map (perm_eq_constr dt_descr sorts perm_fn_frees i) constrs; |
116 |
116 |
117 val perm_eqs = maps perm_eq dt_descr; |
117 val perm_eqs = maps perm_eq dt_descr; |
118 |
118 |
119 val lthy = |
119 val lthy = |
120 Theory_Target.instantiation (user_full_tnames, [], @{sort pt}) thy; |
120 Class.instantiation (user_full_tnames, [], @{sort pt}) thy; |
121 |
121 |
122 val ((perm_funs, perm_eq_thms), lthy') = |
122 val ((perm_funs, perm_eq_thms), lthy') = |
123 Primrec.add_primrec |
123 Primrec.add_primrec |
124 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy; |
124 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy; |
125 |
125 |
138 (map (Morphism.term phi) fvs, map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps); |
138 (map (Morphism.term phi) fvs, map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps); |
139 in |
139 in |
140 lthy' |
140 lthy' |
141 |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms')) |
141 |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms')) |
142 |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms')) |
142 |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms')) |
143 |> Class_Target.prove_instantiation_exit_result morphism tac |
143 |> Class.prove_instantiation_exit_result morphism tac |
144 (perm_funs, perm_eq_thms, perm_zero_thms' @ perm_plus_thms') |
144 (perm_funs, perm_eq_thms, perm_zero_thms' @ perm_plus_thms') |
145 end |
145 end |
146 |
146 |
147 |
147 |
148 end (* structure *) |
148 end (* structure *) |