avoid obsolete Sign.read_prop;
authorwenzelm
Fri Nov 09 19:37:35 2007 +0100 (2007-11-09)
changeset 253654e7a1dabd7ef
parent 25364 7f012f56efa3
child 25366 05c2ae18cc51
avoid obsolete Sign.read_prop;
src/HOL/Tools/inductive_package.ML
src/Provers/blast.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Nov 09 19:37:33 2007 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Nov 09 19:37:35 2007 +0100
     1.3 @@ -413,8 +413,7 @@
     1.4  local
     1.5  
     1.6  (*delete needless equality assumptions*)
     1.7 -val refl_thin = Goal.prove_global HOL.thy [] []
     1.8 -  (Sign.read_prop HOL.thy "!!P. a = a ==> P ==> P")
     1.9 +val refl_thin = Goal.prove_global HOL.thy [] [] @{prop "!!P. a = a ==> P ==> P"}
    1.10    (fn _ => assume_tac 1);
    1.11  val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE];
    1.12  val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
     2.1 --- a/src/Provers/blast.ML	Fri Nov 09 19:37:33 2007 +0100
     2.2 +++ b/src/Provers/blast.ML	Fri Nov 09 19:37:35 2007 +0100
     2.3 @@ -1293,7 +1293,7 @@
     2.4  val fullTrace = ref ([]: branch list list);
     2.5  
     2.6  (*Read a string to make an initial, singleton branch*)
     2.7 -fun readGoal thy s = Sign.read_prop thy s |> fromTerm thy |> rand |> mkGoal;
     2.8 +fun readGoal thy s = Syntax.read_prop_global thy s |> fromTerm thy |> rand |> mkGoal;
     2.9  
    2.10  fun tryInThy thy lim s =
    2.11    let