equal
deleted
inserted
replaced
43 thy |
43 thy |
44 |> Class.instantiation ([tyco], vs, @{sort term_of}) |
44 |> Class.instantiation ([tyco], vs, @{sort term_of}) |
45 |> `(fn lthy => Syntax.check_term lthy eq) |
45 |> `(fn lthy => Syntax.check_term lthy eq) |
46 |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq))) |
46 |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq))) |
47 |> snd |
47 |> snd |
48 |> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) |
48 |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt []) |
49 end; |
49 end; |
50 |
50 |
51 fun ensure_term_of (tyco, (raw_vs, _)) thy = |
51 fun ensure_term_of (tyco, (raw_vs, _)) thy = |
52 let |
52 let |
53 val need_inst = not (Sorts.has_instance (Sign.classes_of thy) tyco @{sort term_of}) |
53 val need_inst = not (Sorts.has_instance (Sign.classes_of thy) tyco @{sort term_of}) |