# HG changeset patch
# User wenzelm
# Date 1164064025 -3600
# Node ID f84cf8e9cad867a58d25a4aaed7adfe9426df4af
# Parent  7c8f4a331f9b3a434b07c1300f507e678f0db267
removed legacy ML setup;

diff -r 7c8f4a331f9b -r f84cf8e9cad8 src/Sequents/LK.thy
--- a/src/Sequents/LK.thy	Tue Nov 21 00:00:39 2006 +0100
+++ b/src/Sequents/LK.thy	Tue Nov 21 00:07:05 2006 +0100
@@ -25,8 +25,6 @@
   left_cong:  "[| P == P';  |- P' ==> ($H |- $F) == ($H' |- $F') |]
                ==> (P, $H |- $F) == (P', $H' |- $F')"
 
-ML {* use_legacy_bindings (the_context ()) *}
-
 use "simpdata.ML"
 
 end
diff -r 7c8f4a331f9b -r f84cf8e9cad8 src/Sequents/LK0.thy
--- a/src/Sequents/LK0.thy	Tue Nov 21 00:00:39 2006 +0100
+++ b/src/Sequents/LK0.thy	Tue Nov 21 00:07:05 2006 +0100
@@ -129,9 +129,6 @@
   If :: "[o, 'a, 'a] => 'a"   ("(if (_)/ then (_)/ else (_))" 10)
    "If(P,x,y) == THE z::'a. (P --> z=x) & (~P --> z=y)"
 
-setup
-  prover_setup
-
 
 (** Structural Rules on formulas **)
 
@@ -240,8 +237,6 @@
                             add_unsafes [thm "allL", thm "exR", thm "the_equality"];
 
 
-pack_ref() := LK_pack;
-
 local
   val thinR = thm "thinR"
   val thinL = thm "thinL"
diff -r 7c8f4a331f9b -r f84cf8e9cad8 src/Sequents/prover.ML
--- a/src/Sequents/prover.ML	Tue Nov 21 00:00:39 2006 +0100
+++ b/src/Sequents/prover.ML	Tue Nov 21 00:07:05 2006 +0100
@@ -166,44 +166,6 @@
   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) 
 	       (step_tac pack 1));
 
-
-
-structure ProverData = TheoryDataFun
-(struct
-  val name = "Sequents/prover";
-  type T = pack ref;
-  val empty = ref empty_pack
-  fun copy (ref pack) = ref pack;
-  val extend = copy;
-  fun merge _ (ref pack1, ref pack2) = ref (merge_pack (pack1, pack2));
-  fun print _ (ref pack) = print_pack pack;
-end);
-
-val prover_setup = ProverData.init;
-
-val print_pack = ProverData.print;
-val pack_ref_of = ProverData.get;
-
-(* access global pack *)
-
-val pack_of = ! o pack_ref_of;
-val pack = pack_of o Context.the_context;
-val pack_ref = pack_ref_of o Context.the_context;
-
-
-(* change global pack *)
-
-fun change_pack f x = pack_ref () := (f (pack (), x));
-
-val Add_safes = change_pack (op add_safes);
-val Add_unsafes = change_pack (op add_unsafes);
-
-
-fun Fast_tac st = fast_tac (pack()) st;
-fun Step_tac st = step_tac (pack()) st;
-fun Safe_tac st = safe_tac (pack()) st;
-fun Pc_tac st   = pc_tac (pack()) st;
-
 end;
 
 
diff -r 7c8f4a331f9b -r f84cf8e9cad8 src/Sequents/simpdata.ML
--- a/src/Sequents/simpdata.ML	Tue Nov 21 00:00:39 2006 +0100
+++ b/src/Sequents/simpdata.ML	Tue Nov 21 00:07:05 2006 +0100
@@ -18,7 +18,7 @@
  (writeln s;
   prove_goal (the_context ()) s
    (fn prems => [ (cut_facts_tac prems 1),
-                  (fast_tac (pack() add_safes [subst]) 1) ]));
+                  (fast_tac (LK_pack add_safes [subst]) 1) ]));
 end;
 
 val conj_simps = map prove_fun
@@ -114,14 +114,14 @@
 
 Goal "|- ~P ==> |- (P <-> False)";
 by (etac (thm "thinR" RS (thm "cut")) 1);
-by (Fast_tac 1);
+by (fast_tac LK_pack 1);
 qed "P_iff_F";
 
 bind_thm ("iff_reflection_F", thm "P_iff_F" RS thm "iff_reflection");
 
 Goal "|- P ==> |- (P <-> True)";
 by (etac (thm "thinR" RS (thm "cut")) 1);
-by (Fast_tac 1);
+by (fast_tac LK_pack 1);
 qed "P_iff_T";
 
 bind_thm ("iff_reflection_T", thm "P_iff_T" RS thm "iff_reflection");
@@ -193,27 +193,27 @@
 val [p1,p2] = Goal
     "[| |- P <-> P';  |- P' ==> |- Q <-> Q' |] ==> |- (P-->Q) <-> (P'-->Q')";
 by (lemma_tac p1 1);
-by (Safe_tac 1);
+by (safe_tac LK_pack 1);
 by (REPEAT (rtac (thm "cut") 1
             THEN
             DEPTH_SOLVE_1 (resolve_tac [thm "thinL", thm "thinR", p2 COMP thm "monotonic"] 1)
             THEN
-            Safe_tac 1));
+            safe_tac LK_pack 1));
 qed "imp_cong";
 
 val [p1,p2] = Goal
     "[| |- P <-> P';  |- P' ==> |- Q <-> Q' |] ==> |- (P&Q) <-> (P'&Q')";
 by (lemma_tac p1 1);
-by (Safe_tac 1);
+by (safe_tac LK_pack 1);
 by (REPEAT (rtac (thm "cut") 1
             THEN
             DEPTH_SOLVE_1 (resolve_tac [thm "thinL", thm "thinR", p2 COMP thm "monotonic"] 1)
             THEN
-            Safe_tac 1));
+            safe_tac LK_pack 1));
 qed "conj_cong";
 
 Goal "|- (x=y) <-> (y=x)";
-by (fast_tac (pack() add_safes [thm "subst"]) 1);
+by (fast_tac (LK_pack add_safes [thm "subst"]) 1);
 qed "eq_sym_conv";
 
 
@@ -251,7 +251,7 @@
 
 val LK_ss =
   LK_basic_ss addsimps LK_simps
-  addeqcongs [left_cong]
+  addeqcongs [thm "left_cong"]
   addcongs [imp_cong];
 
 change_simpset (fn _ => LK_ss);
@@ -269,17 +269,17 @@
 by (simp_tac (simpset() addsimps [thm "if_P"]) 2);
 by (res_inst_tac [ ("P","~Q") ] (thm "cut") 1);
 by (simp_tac (simpset() addsimps [thm "if_not_P"]) 2);
-by (Fast_tac 1);
+by (fast_tac LK_pack 1);
 qed "split_if";
 
 Goal "|- (if P then x else x) = x";
 by (lemma_tac split_if 1);
-by (Fast_tac 1);
+by (fast_tac LK_pack 1);
 qed "if_cancel";
 
 Goal "|- (if x=y then y else x) = x";
 by (lemma_tac split_if 1);
-by (Safe_tac 1);
+by (safe_tac LK_pack 1);
 by (rtac (thm "symL") 1);
 by (rtac (thm "basic") 1);
 qed "if_eq_cancel";