# HG changeset patch
# User wenzelm
# Date 916151153 -3600
# Node ID 3451f9e885285e17d23c9321dac20e26b9588d2a
# Parent  9f75a45384dd41926b842e01121c2cf6fbd0a7dc
eliminated tthm type and Attribute structure;

diff -r 9f75a45384dd -r 3451f9e88528 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Tue Jan 12 15:19:09 1999 +0100
+++ b/src/Provers/classical.ML	Tue Jan 12 15:25:53 1999 +0100
@@ -168,7 +168,7 @@
   val cla_modifiers: (Args.T list -> (Proof.context attribute * Args.T list)) list
   val cla_method: (claset -> tactic) -> Args.src -> Proof.context -> Proof.method
   val cla_method': (claset -> int -> tactic) -> Args.src -> Proof.context -> Proof.method
-  val single_tac: claset -> tthm list -> int -> tactic
+  val single_tac: claset -> thm list -> int -> tactic
   val setup: (theory -> theory) list
 end;
 
@@ -851,10 +851,10 @@
 
 fun change_global_cs f (thy, th) =
   let val r = claset_ref_of thy
-  in r := f (! r, [Attribute.thm_of th]); (thy, th) end;
+  in r := f (! r, [th]); (thy, th) end;
 
 fun change_local_cs f (ctxt, th) =
-  let val cs = f (get_local_claset ctxt, [Attribute.thm_of th])
+  let val cs = f (get_local_claset ctxt, [th])
   in (put_local_claset cs ctxt, th) end;
 
 val haz_dest_global = change_global_cs (op addDs);
@@ -954,10 +954,9 @@
 
 (* single_tac *)
 
-fun single_tac cs tfacts =
+fun single_tac cs facts =
   let
     val CS {safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...} = cs;
-    val facts = Attribute.thms_of tfacts;
     val nets = [safe0_netpair, safep_netpair, haz_netpair, dup_netpair];
     val erules = find_erules facts nets;
 
diff -r 9f75a45384dd -r 3451f9e88528 src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Tue Jan 12 15:19:09 1999 +0100
+++ b/src/Provers/simplifier.ML	Tue Jan 12 15:25:53 1999 +0100
@@ -319,10 +319,10 @@
 
 fun change_global_ss f (thy, th) =
   let val r = simpset_ref_of thy
-  in r := f (! r, [Attribute.thm_of th]); (thy, th) end;
+  in r := f (! r, [th]); (thy, th) end;
 
 fun change_local_ss f (ctxt, th) =
-  let val ss = f (get_local_simpset ctxt, [Attribute.thm_of th])
+  let val ss = f (get_local_simpset ctxt, [th])
   in (put_local_simpset ss ctxt, th) end;
 
 val simp_add_global = change_global_ss (op addsimps);
@@ -422,8 +422,8 @@
 (* conversions *)
 
 fun conv_attr f =
-  (Attrib.no_args (Attribute.rule (f o simpset_of)),
-    Attrib.no_args (Attribute.rule (f o get_local_simpset)));
+  (Attrib.no_args (Drule.rule_attribute (f o simpset_of)),
+    Attrib.no_args (Drule.rule_attribute (f o get_local_simpset)));
 
 
 (* setup_attrs *)
@@ -455,7 +455,7 @@
 
 fun simp_meth tac ctxt = Method.METHOD (fn facts =>
   FIRSTGOAL (REPEAT_DETERM o etac Drule.thin_rl THEN'
-    metacuts_tac (Attribute.thms_of facts) THEN'
+    metacuts_tac facts THEN'
     tac (get_local_simpset ctxt)));
 
 val simp_method = simp_args o simp_meth;