# HG changeset patch
# User wenzelm
# Date 1248466149 -7200
# Node ID 0261c3eaae4110143491d0cc19b0c3600b5ac570
# Parent  bc02c5bfcb5b5b56bc312b12a8c25197bc12dde8
do not open OldGoals;

diff -r bc02c5bfcb5b -r 0261c3eaae41 src/HOL/Modelcheck/MuckeSyn.thy
--- a/src/HOL/Modelcheck/MuckeSyn.thy	Fri Jul 24 21:34:37 2009 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.thy	Fri Jul 24 22:09:09 2009 +0200
@@ -118,7 +118,7 @@
 
 local
 
-  val move_thm = prove_goal @{theory} "[| a = b ==> P a; a = b |] ==> P b"
+  val move_thm = OldGoals.prove_goal @{theory} "[| a = b ==> P a; a = b |] ==> P b"
 	(fn prems => [cut_facts_tac prems 1, dtac sym 1, hyp_subst_tac 1,
 		     REPEAT (resolve_tac prems 1)]);
 
@@ -159,9 +159,9 @@
 
 (* transforming fun-defs into lambda-defs *)
 
-val [eq] = goal Pure.thy "(!! x. f x == g x) ==> f == g";
- by (rtac (extensional eq) 1);
-qed "ext_rl";
+val [eq] = OldGoals.goal Pure.thy "(!! x. f x == g x) ==> f == g";
+ OldGoals.by (rtac (extensional eq) 1);
+OldGoals.qed "ext_rl";
 
 infix cc;
 
@@ -196,7 +196,7 @@
 	val rhs = Syntax.string_of_term_global thy (freeze_thaw RHS)
 	val gl = delete_bold_string (fnam ^" == % " ^ (getargs LHS) ^" . " ^ rhs);
     in
-	SOME (prove_goal thy gl (fn prems =>
+	SOME (OldGoals.prove_goal thy gl (fn prems =>
   		[(REPEAT (rtac ext_rl 1)), (rtac t 1) ]))
     end
 | mk_lam_def [] _ t= NONE; 
diff -r bc02c5bfcb5b -r 0261c3eaae41 src/HOL/Modelcheck/mucke_oracle.ML
--- a/src/HOL/Modelcheck/mucke_oracle.ML	Fri Jul 24 21:34:37 2009 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML	Fri Jul 24 22:09:09 2009 +0200
@@ -1,4 +1,3 @@
-open OldGoals;
 
 val trace_mc = ref false; 
 
@@ -110,9 +109,9 @@
 (
 OldGoals.push_proof();
 OldGoals.goalw_cterm [] (cterm_of sign trm);
-by (simp_tac (global_simpset_of sign) 1);
+OldGoals.by (simp_tac (global_simpset_of sign) 1);
         let
-        val if_tmp_result = result()
+        val if_tmp_result = OldGoals.result()
         in
         (
         OldGoals.pop_proof();
diff -r bc02c5bfcb5b -r 0261c3eaae41 src/HOL/ex/Meson_Test.thy
--- a/src/HOL/ex/Meson_Test.thy	Fri Jul 24 21:34:37 2009 +0200
+++ b/src/HOL/ex/Meson_Test.thy	Fri Jul 24 22:09:09 2009 +0200
@@ -5,7 +5,11 @@
 imports Main
 begin
 
-ML {* open OldGoals *}
+ML {*
+  val Goal = OldGoals.Goal;
+  val by = OldGoals.by;
+  val gethyps = OldGoals.gethyps;
+*}
 
 text {*
   WARNING: there are many potential conflicts between variables used
diff -r bc02c5bfcb5b -r 0261c3eaae41 src/HOLCF/IOA/Modelcheck/MuIOA.thy
--- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Fri Jul 24 21:34:37 2009 +0200
+++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Fri Jul 24 22:09:09 2009 +0200
@@ -246,7 +246,7 @@
 in
 (
 OldGoals.push_proof();
-Goal 
+OldGoals.Goal 
 ( "(Internal_of_A = (% a::(" ^ action_type_str ^ "). a:(" ^ ia_str^
   "))) --> (Internal_of_C = (% a::(" ^ action_type_str ^ "). a:(" ^ ic_str ^ 
   "))) --> (Start_of_A = (% (" ^ abs_pre_tupel_typed ^
@@ -275,21 +275,21 @@
  ") --> (! " ^ con_pre_str_typed ^ ". ! " ^ abs_pre_str_typed ^
 	". (Start_of_C (" ^ con_pre_tupel ^ ") & Start_of_A (" ^ abs_pre_tupel ^
 	")) --> isSimCA(" ^ con_pre_tupel ^ "," ^ abs_pre_tupel ^ "))");
-by (REPEAT (rtac impI 1));
-by (REPEAT (dtac eq_reflection 1));
+OldGoals.by (REPEAT (rtac impI 1));
+OldGoals.by (REPEAT (dtac eq_reflection 1));
 (* Bis hierher wird im Kapitel 4 erl"autert, ab hier im Kapitel 5 *)
-by (full_simp_tac ((global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs)
+OldGoals.by (full_simp_tac ((global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs)
                               delsimps [not_iff,split_part])
 			      addsimps (thl @ comp_simps @ restrict_simps @ hide_simps @
                                         rename_simps @ ioa_simps @ asig_simps)) 1);
-by (full_simp_tac
+OldGoals.by (full_simp_tac
   (Mucke_ss delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1);
-by (REPEAT (if_full_simp_tac
+OldGoals.by (REPEAT (if_full_simp_tac
   (global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1));
-by (call_mucke_tac 1);
+OldGoals.by (call_mucke_tac 1);
 (* Bis hierher wird im Kapitel 5 erl"autert, ab hier wieder im Kapitel 4 *)
-by (atac 1);
-result();
+OldGoals.by (atac 1);
+OldGoals.result();
 OldGoals.pop_proof();
 Thm.cterm_of sign (Logic.strip_imp_concl subgoal)
 )