src/Pure/goal.ML
changeset 50987 616789281413
parent 50974 55f8bd61b029
child 51110 ef0592498418
--- a/src/Pure/goal.ML	Sat Jan 19 21:05:05 2013 +0100
+++ b/src/Pure/goal.ML	Sat Jan 19 22:17:26 2013 +0100
@@ -225,6 +225,7 @@
         Thm.strip_shyps);
     val local_result =
       Thm.future global_result global_prop
+      |> Thm.close_derivation
       |> Thm.instantiate (instT, [])
       |> Drule.forall_elim_list fixes
       |> fold (Thm.elim_implies o Thm.assume) assms;