equal
deleted
inserted
replaced
94 end; |
94 end; |
95 fun perm_eq (i, (_, _, constrs)) = map (perm_eq_constr i) constrs; |
95 fun perm_eq (i, (_, _, constrs)) = map (perm_eq_constr i) constrs; |
96 val perm_eqs = maps perm_eq descr; |
96 val perm_eqs = maps perm_eq descr; |
97 val lthy = |
97 val lthy = |
98 Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; |
98 Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; |
99 (* TODO: Use the version of prmrec that gives the names explicitely. *) |
|
100 val ((perm_frees, perm_ldef), lthy') = |
99 val ((perm_frees, perm_ldef), lthy') = |
101 Primrec.add_primrec |
100 Primrec.add_primrec |
102 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy; |
101 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy; |
103 val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, number); |
102 val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, number); |
104 val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, number) |
103 val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, number) |