src/Pure/Isar/element.ML

--- a/src/Pure/Isar/element.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/Pure/Isar/element.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -268,7 +268,7 @@
 local
 
 val refine_witness =
-  Proof.refine (Method.Basic (K (Method.RAW_METHOD
+  Proof.refine (Method.Basic (K (RAW_METHOD
     (K (ALLGOALS
       (CONJUNCTS (ALLGOALS
         (CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI)))))))), Position.none));