41 val str = Sign.full_name thy name; |
41 val str = Sign.full_name thy name; |
42 |
42 |
43 (* typedef *) |
43 (* typedef *) |
44 val set = atom_decl_set str; |
44 val set = atom_decl_set str; |
45 val tac = rtac @{thm exists_eq_simple_sort} 1; |
45 val tac = rtac @{thm exists_eq_simple_sort} 1; |
46 val ((full_tname, info as {type_definition, Rep_name, Abs_name, ...}), thy) = |
46 val ((full_tname, info as ({Rep_name, Abs_name, ...}, {type_definition, ...})), thy) = |
47 Typedef.add_typedef_global false NONE (name, [], NoSyn) set NONE tac thy; |
47 Typedef.add_typedef_global false NONE (name, [], NoSyn) set NONE tac thy; |
48 |
48 |
49 (* definition of atom and permute *) |
49 (* definition of atom and permute *) |
50 val newT = #abs_type info; |
50 val newT = #abs_type (fst info); |
51 val RepC = Const (Rep_name, newT --> atomT); |
51 val RepC = Const (Rep_name, newT --> atomT); |
52 val AbsC = Const (Abs_name, atomT --> newT); |
52 val AbsC = Const (Abs_name, atomT --> newT); |
53 val a = Free ("a", newT); |
53 val a = Free ("a", newT); |
54 val p = Free ("p", permT); |
54 val p = Free ("p", permT); |
55 val atom_eqn = |
55 val atom_eqn = |