equal
deleted
inserted
replaced
43 (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts) |
43 (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts) |
44 in |
44 in |
45 Thm.instantiate (ctye, []) (forall_intr_vars (forall_intr_frees thm')) |
45 Thm.instantiate (ctye, []) (forall_intr_vars (forall_intr_frees thm')) |
46 end; |
46 end; |
47 |
47 |
48 fun thm_of _ _ (PThm ((name, _), _, prop', SOME Ts)) = |
48 fun thm_of _ _ (PThm (name, _, prop', SOME Ts)) = |
49 let |
49 let |
50 val thm = Drule.implies_intr_hyps (lookup name); |
50 val thm = Drule.implies_intr_hyps (lookup name); |
51 val {prop, ...} = rep_thm thm; |
51 val {prop, ...} = rep_thm thm; |
52 val _ = if prop aconv prop' then () else |
52 val _ = if prop aconv prop' then () else |
53 error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^ |
53 error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^ |