equal
deleted
inserted
replaced
84 end; |
84 end; |
85 |
85 |
86 fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) = |
86 fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) = |
87 let |
87 let |
88 val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name)); |
88 val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name)); |
89 val {prop, ...} = rep_thm thm; |
89 val prop = Thm.prop_of thm; |
90 val _ = |
90 val _ = |
91 if is_equal prop prop' then () |
91 if is_equal prop prop' then () |
92 else |
92 else |
93 error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^ |
93 error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^ |
94 Syntax.string_of_term_global thy prop ^ "\n\n" ^ |
94 Syntax.string_of_term_global thy prop ^ "\n\n" ^ |