equal
deleted
inserted
replaced
38 |
38 |
39 fun thm_of_atom thm Ts = |
39 fun thm_of_atom thm Ts = |
40 let |
40 let |
41 val tvars = term_tvars (prop_of thm); |
41 val tvars = term_tvars (prop_of thm); |
42 val (thm', fmap) = Thm.varifyT' [] thm; |
42 val (thm', fmap) = Thm.varifyT' [] thm; |
43 val ctye = map fst tvars @ map snd fmap ~~ map (Thm.ctyp_of sg) Ts |
43 val ctye = map (pairself (Thm.ctyp_of sg)) |
|
44 (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts) |
44 in |
45 in |
45 Thm.instantiate (ctye, []) (forall_intr_vars (forall_intr_frees thm')) |
46 Thm.instantiate (ctye, []) (forall_intr_vars (forall_intr_frees thm')) |
46 end; |
47 end; |
47 |
48 |
48 fun thm_of _ _ (PThm ((name, _), _, prop', SOME Ts)) = |
49 fun thm_of _ _ (PThm ((name, _), _, prop', SOME Ts)) = |