TFL/rules.ML

--- a/TFL/rules.ML	Sat Jul 08 12:54:32 2006 +0200
+++ b/TFL/rules.ML	Sat Jul 08 12:54:33 2006 +0200
@@ -817,9 +817,9 @@
   let
     val {thy, t, ...} = Thm.rep_cterm ptm;
     val result =
-      if strict then Goal.prove thy [] [] t (K tac)
-      else Goal.prove thy [] [] t (K tac)
+      if strict then Goal.prove_global thy [] [] t (K tac)
+      else Goal.prove_global thy [] [] t (K tac)
         handle ERROR msg => (warning msg; raise RULES_ERR "prove" msg);
-  in #1 (freeze_thaw (standard result)) end;
+  in #1 (freeze_thaw result) end;
 
 end;