equal
deleted
inserted
replaced
53 fun perm_eq (i, (_, _, constrs)) = map (perm_eq_constr i) constrs; |
53 fun perm_eq (i, (_, _, constrs)) = map (perm_eq_constr i) constrs; |
54 val perm_eqs = maps perm_eq descr; |
54 val perm_eqs = maps perm_eq descr; |
55 val lthy = |
55 val lthy = |
56 Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; |
56 Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; |
57 (* TODO: Use the version of prmrec that gives the names explicitely. *) |
57 (* TODO: Use the version of prmrec that gives the names explicitely. *) |
58 val (perm_ldef, lthy') = |
58 val ((_, perm_ldef), lthy') = |
59 Primrec.add_primrec |
59 Primrec.add_primrec |
60 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy; |
60 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy; |
61 val perm_frees = |
61 val perm_frees = |
62 (distinct (op =)) (map (fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) perm_ldef); |
62 (distinct (op =)) (map (fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) perm_ldef); |
63 val perm_empty_thms = |
63 val perm_empty_thms = |