avoid obsolete Sign.read_prop;

--- a/src/HOL/Tools/inductive_package.ML	Fri Nov 09 19:37:33 2007 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Fri Nov 09 19:37:35 2007 +0100
@@ -413,8 +413,7 @@
 local
 
 (*delete needless equality assumptions*)
-val refl_thin = Goal.prove_global HOL.thy [] []
-  (Sign.read_prop HOL.thy "!!P. a = a ==> P ==> P")
+val refl_thin = Goal.prove_global HOL.thy [] [] @{prop "!!P. a = a ==> P ==> P"}
   (fn _ => assume_tac 1);
 val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE];
 val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;

--- 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