changeset 54984 | da70ab8531f4 |
parent 54981 | a128df2f670e |
child 54993 | 625370769fc0 |
--- a/src/Pure/Isar/proof.ML Fri Jan 10 17:44:41 2014 +0100 +++ b/src/Pure/Isar/proof.ML Fri Jan 10 21:37:28 2014 +0100 @@ -492,7 +492,7 @@ handle THM _ => lost_structure ()) |> Drule.flexflex_unique |> Thm.check_shyps (Variable.sorts_of ctxt) - |> Assumption.check_hyps ctxt; + |> Thm.check_hyps ctxt; val goal_propss = filter_out null propss; val results =