src/Pure/Isar/proof.ML

--- a/src/Pure/Isar/proof.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/Pure/Isar/proof.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -780,7 +780,7 @@
   in (rev vars, props') end;
 
 fun refine_terms n =
-  refine (Method.Basic (K (Method.RAW_METHOD
+  refine (Method.Basic (K (RAW_METHOD
     (K (HEADGOAL (PRECISE_CONJUNCTS n
       (HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI)))))))), Position.none))
   #> Seq.hd;