equal
deleted
inserted
replaced
26 fun is_datatype (Type (a, _)) = Long_Name.base_name a = Long_Name.base_name datatype_name |
26 fun is_datatype (Type (a, _)) = Long_Name.base_name a = Long_Name.base_name datatype_name |
27 | is_datatype _ = false; |
27 | is_datatype _ = false; |
28 |
28 |
29 val datatype_var = |
29 val datatype_var = |
30 (case find_first (fn (_, T') => is_datatype T') vars of |
30 (case find_first (fn (_, T') => is_datatype T') vars of |
31 SOME var => Thm.cterm_of ctxt (Term.Var var) |
31 SOME (xi, _) => xi |
32 | NONE => error ("Couldn't find datatype in thm: " ^ datatype_name)); |
32 | NONE => error ("Couldn't find datatype in thm: " ^ datatype_name)); |
33 in |
33 in |
34 SOME (Drule.cterm_instantiate [(datatype_var, Thm.cterm_of ctxt (List.last args))] split) |
34 SOME (infer_instantiate ctxt [(datatype_var, Thm.cterm_of ctxt (List.last args))] split) |
35 end |
35 end |
36 handle TERM _ => NONE; |
36 handle TERM _ => NONE; |
37 \<close> |
37 \<close> |
38 |
38 |
39 end |
39 end |