src/Provers/blast.ML
changeset 25365 4e7a1dabd7ef
parent 24112 6c4e7d17f9b0
child 26928 ca87aff1ad2d
--- a/src/Provers/blast.ML	Fri Nov 09 19:37:33 2007 +0100
+++ b/src/Provers/blast.ML	Fri Nov 09 19:37:35 2007 +0100
@@ -1293,7 +1293,7 @@
 val fullTrace = ref ([]: branch list list);
 
 (*Read a string to make an initial, singleton branch*)
-fun readGoal thy s = Sign.read_prop thy s |> fromTerm thy |> rand |> mkGoal;
+fun readGoal thy s = Syntax.read_prop_global thy s |> fromTerm thy |> rand |> mkGoal;
 
 fun tryInThy thy lim s =
   let