prefer antiquotations;
authorwenzelm
Tue Apr 05 17:25:11 2016 +0200 (2016-04-05)
changeset 62870cf724647f75b
parent 62869 64a5cf42be1e
child 62871 4a6cbe1239fe
prefer antiquotations;
src/HOL/Matrix_LP/Compute_Oracle/compute.ML
src/Provers/splitter.ML
src/Pure/ML/ml_pervasive_final.ML
src/Pure/ROOT.ML
     1.1 --- a/src/HOL/Matrix_LP/Compute_Oracle/compute.ML	Tue Apr 05 17:16:46 2016 +0200
     1.2 +++ b/src/HOL/Matrix_LP/Compute_Oracle/compute.ML	Tue Apr 05 17:25:11 2016 +0200
     1.3 @@ -582,7 +582,7 @@
     1.4              case match_aterms varsubst b' a' of
     1.5                  NONE => 
     1.6                  let
     1.7 -                    fun mk s = Syntax.string_of_term_global Pure.thy
     1.8 +                    fun mk s = Syntax.string_of_term_global @{theory Pure}
     1.9                        (infer_types (naming_of computer) (encoding_of computer) ty s)
    1.10                      val left = "computed left side: "^(mk a')
    1.11                      val right = "computed right side: "^(mk b')
     2.1 --- a/src/Provers/splitter.ML	Tue Apr 05 17:16:46 2016 +0200
     2.2 +++ b/src/Provers/splitter.ML	Tue Apr 05 17:25:11 2016 +0200
     2.3 @@ -98,9 +98,9 @@
     2.4  
     2.5  val meta_iffD = Data.meta_eq_to_iff RS Data.iffD;  (* (P == Q) ==> Q ==> P *)
     2.6  
     2.7 -val lift = Goal.prove_global Pure.thy ["P", "Q", "R"]
     2.8 -  [Syntax.read_prop_global Pure.thy "!!x :: 'b. Q(x) == R(x) :: 'c"]
     2.9 -  (Syntax.read_prop_global Pure.thy "P(%x. Q(x)) == P(%x. R(x))")
    2.10 +val lift = Goal.prove_global @{theory Pure} ["P", "Q", "R"]
    2.11 +  [Syntax.read_prop_global @{theory Pure} "!!x :: 'b. Q(x) == R(x) :: 'c"]
    2.12 +  (Syntax.read_prop_global @{theory Pure} "P(%x. Q(x)) == P(%x. R(x))")
    2.13    (fn {context = ctxt, prems} =>
    2.14      rewrite_goals_tac ctxt prems THEN resolve_tac ctxt [reflexive_thm] 1)
    2.15  
     3.1 --- a/src/Pure/ML/ml_pervasive_final.ML	Tue Apr 05 17:16:46 2016 +0200
     3.2 +++ b/src/Pure/ML/ml_pervasive_final.ML	Tue Apr 05 17:25:11 2016 +0200
     3.3 @@ -11,8 +11,6 @@
     3.4  
     3.5  structure Output: OUTPUT = Output;  (*seal system channels!*)
     3.6  
     3.7 -structure Pure = struct val thy = Thy_Info.pure_theory () end;
     3.8 -
     3.9  Proofterm.proofs := 0;
    3.10  
    3.11  Context.set_thread_data NONE;
     4.1 --- a/src/Pure/ROOT.ML	Tue Apr 05 17:16:46 2016 +0200
     4.2 +++ b/src/Pure/ROOT.ML	Tue Apr 05 17:25:11 2016 +0200
     4.3 @@ -226,7 +226,7 @@
     4.4  
     4.5  
     4.6  
     4.7 -(** bootstrap phase 3: towards Pure.thy and final ML toplevel setup *)
     4.8 +(** bootstrap phase 3: towards theory "Pure" and final ML toplevel setup *)
     4.9  
    4.10  (*basic proof engine*)
    4.11  use "par_tactical.ML";