| 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