equal
deleted
inserted
replaced
54 val rhs = @{term Typerep} $ HOLogic.mk_literal tyco |
54 val rhs = @{term Typerep} $ HOLogic.mk_literal tyco |
55 $ HOLogic.mk_list @{typ typerep} (map (HOLogic.mk_typerep o TFree) vs); |
55 $ HOLogic.mk_list @{typ typerep} (map (HOLogic.mk_typerep o TFree) vs); |
56 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); |
56 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); |
57 in |
57 in |
58 thy |
58 thy |
59 |> Theory_Target.instantiation ([tyco], vs, @{sort typerep}) |
59 |> Class.instantiation ([tyco], vs, @{sort typerep}) |
60 |> `(fn lthy => Syntax.check_term lthy eq) |
60 |> `(fn lthy => Syntax.check_term lthy eq) |
61 |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq))) |
61 |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq))) |
62 |> snd |
62 |> snd |
63 |> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) |
63 |> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) |
64 end; |
64 end; |