--- 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')
--- 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)
--- 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;
--- 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";