src/Pure/Proof/extraction.ML

 );
 
 fun read_condeq thy =
   let val thy' = add_syntax thy
   in fn s =>
-    let val t = Logic.varify (Sign.read_prop thy' s)
+    let val t = Logic.varify (Syntax.read_prop_global thy' s)
     in (map Logic.dest_equals (Logic.strip_imp_prems t),
       Logic.dest_equals (Logic.strip_imp_concl t))
     end handle TERM _ => error ("Not a (conditional) meta equality:\n" ^ s)
   end;