# HG changeset patch
# User wenzelm
# Date 1459869911 -7200
# Node ID cf724647f75b9af8c1a284720ca4ae807a8cb9c1
# Parent  64a5cf42be1ea7b41a652b7542abe3a6447888d3
prefer antiquotations;

diff -r 64a5cf42be1e -r cf724647f75b src/HOL/Matrix_LP/Compute_Oracle/compute.ML
--- a/src/HOL/Matrix_LP/Compute_Oracle/compute.ML	Tue Apr 05 17:16:46 2016 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/compute.ML	Tue Apr 05 17:25:11 2016 +0200
@@ -582,7 +582,7 @@
             case match_aterms varsubst b' a' of
                 NONE => 
                 let
-                    fun mk s = Syntax.string_of_term_global Pure.thy
+                    fun mk s = Syntax.string_of_term_global @{theory Pure}
                       (infer_types (naming_of computer) (encoding_of computer) ty s)
                     val left = "computed left side: "^(mk a')
                     val right = "computed right side: "^(mk b')
diff -r 64a5cf42be1e -r cf724647f75b src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Tue Apr 05 17:16:46 2016 +0200
+++ b/src/Provers/splitter.ML	Tue Apr 05 17:25:11 2016 +0200
@@ -98,9 +98,9 @@
 
 val meta_iffD = Data.meta_eq_to_iff RS Data.iffD;  (* (P == Q) ==> Q ==> P *)
 
-val lift = Goal.prove_global Pure.thy ["P", "Q", "R"]
-  [Syntax.read_prop_global Pure.thy "!!x :: 'b. Q(x) == R(x) :: 'c"]
-  (Syntax.read_prop_global Pure.thy "P(%x. Q(x)) == P(%x. R(x))")
+val lift = Goal.prove_global @{theory Pure} ["P", "Q", "R"]
+  [Syntax.read_prop_global @{theory Pure} "!!x :: 'b. Q(x) == R(x) :: 'c"]
+  (Syntax.read_prop_global @{theory Pure} "P(%x. Q(x)) == P(%x. R(x))")
   (fn {context = ctxt, prems} =>
     rewrite_goals_tac ctxt prems THEN resolve_tac ctxt [reflexive_thm] 1)
 
diff -r 64a5cf42be1e -r cf724647f75b src/Pure/ML/ml_pervasive_final.ML
--- a/src/Pure/ML/ml_pervasive_final.ML	Tue Apr 05 17:16:46 2016 +0200
+++ b/src/Pure/ML/ml_pervasive_final.ML	Tue Apr 05 17:25:11 2016 +0200
@@ -11,8 +11,6 @@
 
 structure Output: OUTPUT = Output;  (*seal system channels!*)
 
-structure Pure = struct val thy = Thy_Info.pure_theory () end;
-
 Proofterm.proofs := 0;
 
 Context.set_thread_data NONE;
diff -r 64a5cf42be1e -r cf724647f75b src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Apr 05 17:16:46 2016 +0200
+++ b/src/Pure/ROOT.ML	Tue Apr 05 17:25:11 2016 +0200
@@ -226,7 +226,7 @@
 
 
 
-(** bootstrap phase 3: towards Pure.thy and final ML toplevel setup *)
+(** bootstrap phase 3: towards theory "Pure" and final ML toplevel setup *)
 
 (*basic proof engine*)
 use "par_tactical.ML";