equal
deleted
inserted
replaced
54 "_triv" |
54 "_triv" |
55 in |
55 in |
56 thy |
56 thy |
57 |> Class.instantiation ([tyco], vs, @{sort partial_term_of}) |
57 |> Class.instantiation ([tyco], vs, @{sort partial_term_of}) |
58 |> `(fn lthy => Syntax.check_term lthy eq) |
58 |> `(fn lthy => Syntax.check_term lthy eq) |
59 |-> (fn eq => Specification.definition NONE [] ((Binding.name (triv_name_of eq), []), eq)) |
59 |-> (fn eq => Specification.definition NONE [] [] ((Binding.name (triv_name_of eq), []), eq)) |
60 |> snd |
60 |> snd |
61 |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt []) |
61 |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt []) |
62 end |
62 end |
63 |
63 |
64 fun ensure_partial_term_of (tyco, (raw_vs, _)) thy = |
64 fun ensure_partial_term_of (tyco, (raw_vs, _)) thy = |