explicit OldGoals;
authorwenzelm
Fri Jul 24 21:02:34 2009 +0200 (2009-07-24)
changeset 321749036cc8ae775
parent 32173 34f7b0fbe047
child 32175 a89979440d2c
explicit OldGoals;
src/CCL/CCL.thy
src/HOL/Import/proof_kernel.ML
src/HOL/Modelcheck/mucke_oracle.ML
src/HOL/ex/Meson_Test.thy
src/Provers/blast.ML
src/Provers/splitter.ML
     1.1 --- a/src/CCL/CCL.thy	Fri Jul 24 20:55:56 2009 +0200
     1.2 +++ b/src/CCL/CCL.thy	Fri Jul 24 21:02:34 2009 +0200
     1.3 @@ -256,12 +256,12 @@
     1.4  
     1.5  val ccl_dstncts =
     1.6          let fun mk_raw_dstnct_thm rls s =
     1.7 -                  prove_goal @{theory} s (fn _=> [rtac notI 1,eresolve_tac rls 1])
     1.8 +                  OldGoals.prove_goal @{theory} s (fn _=> [rtac notI 1,eresolve_tac rls 1])
     1.9          in map (mk_raw_dstnct_thm caseB_lemmas)
    1.10                  (mk_dstnct_rls @{theory} ["bot","true","false","pair","lambda"]) end
    1.11  
    1.12  fun mk_dstnct_thms thy defs inj_rls xs =
    1.13 -  let fun mk_dstnct_thm rls s = prove_goalw thy defs s
    1.14 +  let fun mk_dstnct_thm rls s = OldGoals.prove_goalw thy defs s
    1.15      (fn _ => [simp_tac (global_simpset_of thy addsimps (rls@inj_rls)) 1])
    1.16    in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end
    1.17  
     2.1 --- a/src/HOL/Import/proof_kernel.ML	Fri Jul 24 20:55:56 2009 +0200
     2.2 +++ b/src/HOL/Import/proof_kernel.ML	Fri Jul 24 21:02:34 2009 +0200
     2.3 @@ -245,7 +245,7 @@
     2.4  
     2.5  fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm_without_context th)
     2.6  fun prc ct = writeln (PrintMode.setmp [] Display.string_of_cterm ct)
     2.7 -fun prin t = writeln (PrintMode.setmp [] (fn () => Syntax.string_of_term_global (the_context ()) t) ());
     2.8 +fun prin t = writeln (PrintMode.setmp [] (fn () => Syntax.string_of_term_global (OldGoals.the_context ()) t) ());
     2.9  fun pth (HOLThm(ren,thm)) =
    2.10      let
    2.11          (*val _ = writeln "Renaming:"
     3.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Fri Jul 24 20:55:56 2009 +0200
     3.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Fri Jul 24 21:02:34 2009 +0200
     3.3 @@ -1,3 +1,4 @@
     3.4 +open OldGoals;
     3.5  
     3.6  val trace_mc = ref false; 
     3.7  
     4.1 --- a/src/HOL/ex/Meson_Test.thy	Fri Jul 24 20:55:56 2009 +0200
     4.2 +++ b/src/HOL/ex/Meson_Test.thy	Fri Jul 24 21:02:34 2009 +0200
     4.3 @@ -5,6 +5,8 @@
     4.4  imports Main
     4.5  begin
     4.6  
     4.7 +ML {* open OldGoals *}
     4.8 +
     4.9  text {*
    4.10    WARNING: there are many potential conflicts between variables used
    4.11    below and constants declared in HOL!
     5.1 --- a/src/Provers/blast.ML	Fri Jul 24 20:55:56 2009 +0200
     5.2 +++ b/src/Provers/blast.ML	Fri Jul 24 21:02:34 2009 +0200
     5.3 @@ -181,8 +181,8 @@
     5.4  fun isGoal (Const ("*Goal*", _) $ _) = true
     5.5    | isGoal _ = false;
     5.6  
     5.7 -val TruepropC = ObjectLogic.judgment_name (the_context ());
     5.8 -val TruepropT = Sign.the_const_type (the_context ()) TruepropC;
     5.9 +val TruepropC = ObjectLogic.judgment_name (OldGoals.the_context ());
    5.10 +val TruepropT = Sign.the_const_type (OldGoals.the_context ()) TruepropC;
    5.11  
    5.12  fun mk_Trueprop t = Term.$ (Term.Const (TruepropC, TruepropT), t);
    5.13  
     6.1 --- a/src/Provers/splitter.ML	Fri Jul 24 20:55:56 2009 +0200
     6.2 +++ b/src/Provers/splitter.ML	Fri Jul 24 21:02:34 2009 +0200
     6.3 @@ -1,5 +1,4 @@
     6.4 -(*  Title:      Provers/splitter
     6.5 -    ID:         $Id$
     6.6 +(*  Title:      Provers/splitter.ML
     6.7      Author:     Tobias Nipkow
     6.8      Copyright   1995  TU Munich
     6.9  
    6.10 @@ -45,14 +44,14 @@
    6.11  struct
    6.12  
    6.13  val Const (const_not, _) $ _ =
    6.14 -  ObjectLogic.drop_judgment (the_context ())
    6.15 +  ObjectLogic.drop_judgment (OldGoals.the_context ())
    6.16      (#1 (Logic.dest_implies (Thm.prop_of Data.notnotD)));
    6.17  
    6.18  val Const (const_or , _) $ _ $ _ =
    6.19 -  ObjectLogic.drop_judgment (the_context ())
    6.20 +  ObjectLogic.drop_judgment (OldGoals.the_context ())
    6.21      (#1 (Logic.dest_implies (Thm.prop_of Data.disjE)));
    6.22  
    6.23 -val const_Trueprop = ObjectLogic.judgment_name (the_context ());
    6.24 +val const_Trueprop = ObjectLogic.judgment_name (OldGoals.the_context ());
    6.25  
    6.26  
    6.27  fun split_format_err () = error "Wrong format for split rule";