removed obsolete delta stuff;

--- a/src/Provers/classical.ML	Wed Jul 13 16:07:26 2005 +0200
+++ b/src/Provers/classical.ML	Wed Jul 13 16:07:27 2005 +0200
@@ -14,13 +14,6 @@
 the conclusion.
 *)
 
-
-(*added: get_delta_claset, put_delta_claset.
-        changed: safe_{dest,elim,intro}_local and haz_{dest,elim,intro}_local
-   06/01/05
-*)
-
-
 (*higher precedence than := facilitates use of references*)
 infix 4 addSIs addSEs addSDs addIs addEs addDs delrules
   addSWrapper delSWrapper addWrapper delWrapper
@@ -171,10 +164,6 @@
   val cla_method: (claset -> tactic) -> Method.src -> Proof.context -> Proof.method
   val cla_method': (claset -> int -> tactic) -> Method.src -> Proof.context -> Proof.method
   val setup: (theory -> theory) list
-
-  val get_delta_claset: ProofContext.context -> claset
-  val put_delta_claset: claset -> ProofContext.context -> ProofContext.context
-
 end;
 
 
@@ -899,41 +888,6 @@
 fun local_claset_of ctxt =
   context_cs ctxt (get_local_claset ctxt) (get_context_cs ctxt);
 
-(* added for delta_claset: 06/01/05 *)
-(* CB: changed "delta clasets" to context data,
-       moved counter to here, it is no longer a ref *)
-
-structure DeltaClasetArgs =
-struct
-  val name = "Provers/delta_claset";
-  type T = claset * int;
-  fun init _ = (empty_cs, 0)
-  fun print ctxt cs = ();
-end;
-
-structure DeltaClasetData = ProofDataFun(DeltaClasetArgs);
-val get_delta_claset = #1 o DeltaClasetData.get;
-fun put_delta_claset cs = DeltaClasetData.map (fn (_, i) => (cs, i));
-fun delta_increment ctxt =
-  let val ctxt' = DeltaClasetData.map (fn (ss, i) => (ss, i+1)) ctxt
-  in (ctxt', #2 (DeltaClasetData.get ctxt'))
-  end;
-
-local
-fun rename_thm' (ctxt,thm) =
-  let val (new_ctxt, new_id) = delta_increment ctxt
-      val new_name = "anon_cla_" ^ (string_of_int new_id)
-  in
-    (new_ctxt, Thm.name_thm(new_name,thm))
-end;
-
-in
-
-(* rename thm if call_atp is true *)
-fun rename_thm (ctxt,thm) = if (!Proof.call_atp) then rename_thm' (ctxt,thm) else (ctxt, thm);
-
-end
-
 
 (* attributes *)
 
@@ -953,70 +907,12 @@
 val haz_intro_global = change_global_cs (op addIs);
 val rule_del_global = change_global_cs (op delrules) o ContextRules.rule_del_global;
 
-
-(* when dest/elim/intro rules are added to local_claset, they are also added to delta_claset in ProofContext.context *)
-fun safe_dest_local (ctxt,th) =
-    let val thm_name = Thm.name_of_thm th
-        val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th)  else (ctxt, th)
-        val delta_cs = get_delta_claset ctxt'
-        val new_dcs = delta_cs addSDs [th']
-        val ctxt'' = put_delta_claset new_dcs ctxt'
-    in
-        change_local_cs (op addSDs) (ctxt'',th)
-    end;
-
-fun safe_elim_local (ctxt, th)=
-    let val thm_name = Thm.name_of_thm th
-        val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, th)
-        val delta_cs = get_delta_claset ctxt'
-        val new_dcs = delta_cs addSEs [th']
-        val ctxt'' = put_delta_claset new_dcs ctxt'
-    in
-        change_local_cs (op addSEs) (ctxt'',th)
-    end;
-
-fun safe_intro_local (ctxt, th) =
-    let val thm_name = Thm.name_of_thm th
-        val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, th)
-        val delta_cs = get_delta_claset ctxt'
-        val new_dcs = delta_cs addSIs [th']
-        val ctxt'' = put_delta_claset new_dcs ctxt'
-    in
-        change_local_cs (op addSIs) (ctxt'',th)
-    end;
-
-fun haz_dest_local (ctxt, th)=
-    let val thm_name = Thm.name_of_thm th
-        val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th)else (ctxt, th)
-        val delta_cs = get_delta_claset ctxt'
-        val new_dcs = delta_cs addDs [th']
-        val ctxt'' = put_delta_claset new_dcs ctxt'
-    in
-        change_local_cs (op addDs) (ctxt'',th)
-    end;
-
-fun haz_elim_local (ctxt,th) =
-    let val thm_name = Thm.name_of_thm th
-        val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th)  else (ctxt, th)
-        val delta_cs = get_delta_claset ctxt'
-        val new_dcs = delta_cs addEs [th']
-        val ctxt'' = put_delta_claset new_dcs ctxt'
-    in
-        change_local_cs (op addEs) (ctxt'',th)
-    end;
-
-fun haz_intro_local (ctxt,th) =
-    let val thm_name = Thm.name_of_thm th
-        val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th)  else (ctxt, th)
-        val delta_cs = get_delta_claset ctxt'
-        val new_dcs = delta_cs addIs [th']
-        val ctxt'' = put_delta_claset new_dcs ctxt'
-    in
-        change_local_cs (op addIs) (ctxt'',th)
-    end;
-
-
-(* when a rule is removed from local_claset, it is not removed from delta_claset in ProofContext.context.  But this is unlikely to happen. *)
+val safe_dest_local = change_local_cs (op addSDs);
+val safe_elim_local = change_local_cs (op addSEs);
+val safe_intro_local = change_local_cs (op addSIs);
+val haz_dest_local = change_local_cs (op addDs);
+val haz_elim_local = change_local_cs (op addEs);
+val haz_intro_local = change_local_cs (op addIs);
 val rule_del_local = change_local_cs (op delrules) o ContextRules.rule_del_local;
 
 
@@ -1158,8 +1054,7 @@
 
 (** theory setup **)
 
-val setup = [GlobalClaset.init, LocalClaset.init, DeltaClasetData.init,
-  setup_attrs, setup_methods];
+val setup = [GlobalClaset.init, LocalClaset.init, setup_attrs, setup_methods];
 
 
 
@@ -1175,4 +1070,3 @@
 
 
 end;
-

--- a/src/Pure/simplifier.ML	Wed Jul 13 16:07:26 2005 +0200
+++ b/src/Pure/simplifier.ML	Wed Jul 13 16:07:27 2005 +0200
@@ -6,12 +6,6 @@
 meta_simplifier.ML for the actual meta-level rewriting engine).
 *)
 
-(* added: put_delta_simpset, get_delta_simpset
-   changed: simp_add_local
-   07/01/05
-*)
-
-
 signature BASIC_SIMPLIFIER =
 sig
   include BASIC_META_SIMPLIFIER
@@ -98,9 +92,6 @@
   val method_setup: (Args.T list -> (Method.modifier * Args.T list)) list
     -> (theory -> theory) list
   val easy_setup: thm -> thm list -> (theory -> theory) list
-
-  val get_delta_simpset: ProofContext.context -> Thm.thm list
-  val put_delta_simpset: Thm.thm list -> ProofContext.context -> ProofContext.context
 end;
 
 structure Simplifier: SIMPLIFIER =
@@ -134,7 +125,7 @@
   mk_context_simproc name o map (Thm.cterm_of thy o Logic.varify);
 
 fun context_simproc thy name =
-  context_simproc_i thy name o map (Sign.simple_read_term thy TypeInfer.logicT);
+  context_simproc_i thy name o map (Sign.read_term thy);
 
 
 (* datatype context_ss *)
@@ -303,44 +294,6 @@
   context_ss ctxt (get_local_simpset ctxt) (get_context_ss ctxt);
 
 
-(* Jia: added DeltaSimpsetArgs and DeltaSimpset for delta_simpset
-	also added methods to retrieve them. *)
-(* CB: changed "delta simpsets" to context data,
-       moved counter to here, it is no longer a ref *)
-
-structure DeltaSimpsetArgs =
-struct
-  val name = "Pure/delta_simpset";
-  type T = Thm.thm list * int;  (*the type is thm list * int*)
-  fun init _ = ([], 0);
-  fun print ctxt thms = ();
-end;
-
-structure DeltaSimpsetData = ProofDataFun(DeltaSimpsetArgs);
-val _ = Context.add_setup [DeltaSimpsetData.init];
-
-val get_delta_simpset = #1 o DeltaSimpsetData.get;
-fun put_delta_simpset ss = DeltaSimpsetData.map (fn (_, i) => (ss, i));
-fun delta_increment ctxt =
-  let val ctxt' = DeltaSimpsetData.map (fn (ss, i) => (ss, i+1)) ctxt
-  in (ctxt', #2 (DeltaSimpsetData.get ctxt'))
-  end;
-
-(* Jia: added to rename a local thm if necessary *) 
-local 
-fun rename_thm' (ctxt,thm) =
-  let val (new_ctxt, new_id) = delta_increment ctxt
-      val new_name = "anon_simp_" ^ (string_of_int new_id)
-  in
-    (new_ctxt, Thm.name_thm(new_name,thm))
-end;
-
-in
-
-fun rename_thm (ctxt,thm) = if (!Proof.call_atp) then rename_thm' (ctxt,thm) else (ctxt, thm);
-
-end
-
 (* attributes *)
 
 fun change_global_ss f (thy, th) =
@@ -353,23 +306,7 @@
 
 val simp_add_global = change_global_ss (op addsimps);
 val simp_del_global = change_global_ss (op delsimps);
-
-
-
-
-
-(* Jia: note: when simplifier rules are added to local_simpset, they are also added to delta_simpset in ProofContext.context, but not removed if simp_del_local is called *)
-fun simp_add_local (ctxt,th) = 
-    let val delta_ss = get_delta_simpset ctxt
-	val thm_name = Thm.name_of_thm th
-        val (ctxt', th') =
-          if (thm_name = "") then rename_thm (ctxt,th)  else (ctxt, th)
-	val new_dss = th'::delta_ss
-	val ctxt'' = put_delta_simpset new_dss ctxt' 
-    in
-	change_local_ss (op addsimps) (ctxt'',th)
-    end;
-
+val simp_add_local = change_local_ss (op addsimps);
 val simp_del_local = change_local_ss (op delsimps);
 
 val cong_add_global = change_global_ss (op addcongs);
@@ -378,6 +315,8 @@
 val cong_del_local = change_local_ss (op delcongs);
 
 
+(* tactics *)
+
 val simp_tac = generic_simp_tac false (false, false, false);
 val asm_simp_tac = generic_simp_tac false (false, true, false);
 val full_simp_tac = generic_simp_tac false (true, false, false);
@@ -385,8 +324,6 @@
 val asm_full_simp_tac = generic_simp_tac false (true, true, true);
 val safe_asm_full_simp_tac = generic_simp_tac true (true, true, true);
 
-
-
 (*the abstraction over the proof state delays the dereferencing*)
 fun          Simp_tac i st =          simp_tac (simpset ()) i st;
 fun      Asm_simp_tac i st =      asm_simp_tac (simpset ()) i st;
@@ -394,6 +331,9 @@
 fun   Asm_lr_simp_tac i st =   asm_lr_simp_tac (simpset ()) i st;
 fun Asm_full_simp_tac i st = asm_full_simp_tac (simpset ()) i st;
 
+
+(* conversions *)
+
 val          simplify = simp_thm (false, false, false);
 val      asm_simplify = simp_thm (false, true, false);
 val     full_simplify = simp_thm (true, false, false);