# HG changeset patch
# User wenzelm
# Date 1248462154 -7200
# Node ID 9036cc8ae7757cb13da2ebdb3efe06a52626d7ca
# Parent  34f7b0fbe047f516b5dd6de8738ae2c9831be14e
explicit OldGoals;

diff -r 34f7b0fbe047 -r 9036cc8ae775 src/CCL/CCL.thy
--- a/src/CCL/CCL.thy	Fri Jul 24 20:55:56 2009 +0200
+++ b/src/CCL/CCL.thy	Fri Jul 24 21:02:34 2009 +0200
@@ -256,12 +256,12 @@
 
 val ccl_dstncts =
         let fun mk_raw_dstnct_thm rls s =
-                  prove_goal @{theory} s (fn _=> [rtac notI 1,eresolve_tac rls 1])
+                  OldGoals.prove_goal @{theory} s (fn _=> [rtac notI 1,eresolve_tac rls 1])
         in map (mk_raw_dstnct_thm caseB_lemmas)
                 (mk_dstnct_rls @{theory} ["bot","true","false","pair","lambda"]) end
 
 fun mk_dstnct_thms thy defs inj_rls xs =
-  let fun mk_dstnct_thm rls s = prove_goalw thy defs s
+  let fun mk_dstnct_thm rls s = OldGoals.prove_goalw thy defs s
     (fn _ => [simp_tac (global_simpset_of thy addsimps (rls@inj_rls)) 1])
   in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end
 
diff -r 34f7b0fbe047 -r 9036cc8ae775 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Fri Jul 24 20:55:56 2009 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Fri Jul 24 21:02:34 2009 +0200
@@ -245,7 +245,7 @@
 
 fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm_without_context th)
 fun prc ct = writeln (PrintMode.setmp [] Display.string_of_cterm ct)
-fun prin t = writeln (PrintMode.setmp [] (fn () => Syntax.string_of_term_global (the_context ()) t) ());
+fun prin t = writeln (PrintMode.setmp [] (fn () => Syntax.string_of_term_global (OldGoals.the_context ()) t) ());
 fun pth (HOLThm(ren,thm)) =
     let
         (*val _ = writeln "Renaming:"
diff -r 34f7b0fbe047 -r 9036cc8ae775 src/HOL/Modelcheck/mucke_oracle.ML
--- a/src/HOL/Modelcheck/mucke_oracle.ML	Fri Jul 24 20:55:56 2009 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML	Fri Jul 24 21:02:34 2009 +0200
@@ -1,3 +1,4 @@
+open OldGoals;
 
 val trace_mc = ref false; 
 
diff -r 34f7b0fbe047 -r 9036cc8ae775 src/HOL/ex/Meson_Test.thy
--- a/src/HOL/ex/Meson_Test.thy	Fri Jul 24 20:55:56 2009 +0200
+++ b/src/HOL/ex/Meson_Test.thy	Fri Jul 24 21:02:34 2009 +0200
@@ -5,6 +5,8 @@
 imports Main
 begin
 
+ML {* open OldGoals *}
+
 text {*
   WARNING: there are many potential conflicts between variables used
   below and constants declared in HOL!
diff -r 34f7b0fbe047 -r 9036cc8ae775 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Fri Jul 24 20:55:56 2009 +0200
+++ b/src/Provers/blast.ML	Fri Jul 24 21:02:34 2009 +0200
@@ -181,8 +181,8 @@
 fun isGoal (Const ("*Goal*", _) $ _) = true
   | isGoal _ = false;
 
-val TruepropC = ObjectLogic.judgment_name (the_context ());
-val TruepropT = Sign.the_const_type (the_context ()) TruepropC;
+val TruepropC = ObjectLogic.judgment_name (OldGoals.the_context ());
+val TruepropT = Sign.the_const_type (OldGoals.the_context ()) TruepropC;
 
 fun mk_Trueprop t = Term.$ (Term.Const (TruepropC, TruepropT), t);
 
diff -r 34f7b0fbe047 -r 9036cc8ae775 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Fri Jul 24 20:55:56 2009 +0200
+++ b/src/Provers/splitter.ML	Fri Jul 24 21:02:34 2009 +0200
@@ -1,5 +1,4 @@
-(*  Title:      Provers/splitter
-    ID:         $Id$
+(*  Title:      Provers/splitter.ML
     Author:     Tobias Nipkow
     Copyright   1995  TU Munich
 
@@ -45,14 +44,14 @@
 struct
 
 val Const (const_not, _) $ _ =
-  ObjectLogic.drop_judgment (the_context ())
+  ObjectLogic.drop_judgment (OldGoals.the_context ())
     (#1 (Logic.dest_implies (Thm.prop_of Data.notnotD)));
 
 val Const (const_or , _) $ _ $ _ =
-  ObjectLogic.drop_judgment (the_context ())
+  ObjectLogic.drop_judgment (OldGoals.the_context ())
     (#1 (Logic.dest_implies (Thm.prop_of Data.disjE)));
 
-val const_Trueprop = ObjectLogic.judgment_name (the_context ());
+val const_Trueprop = ObjectLogic.judgment_name (OldGoals.the_context ());
 
 
 fun split_format_err () = error "Wrong format for split rule";