# HG changeset patch
# User wenzelm
# Date 1205963258 -3600
# Node ID a85fe32e7b2f52e0ce076585030855f294535402
# Parent  7825c83c9efff5d358abea0c57fa46b408c2c348
more antiquotations;
eliminated change_claset/simpset;

diff -r 7825c83c9eff -r a85fe32e7b2f src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Mar 19 22:47:35 2008 +0100
+++ b/src/HOL/Product_Type.thy	Wed Mar 19 22:47:38 2008 +0100
@@ -322,7 +322,7 @@
   ?P(a, b)"} which cannot be solved by reflexivity.
 *}
 
-ML_setup {*
+ML {*
   (* replace parameters of product type by individual component parameters *)
   val safe_full_simp_tac = generic_simp_tac true (true, false, false);
   local (* filtering with exists_paired_all is an essential optimization *)
@@ -332,7 +332,7 @@
       | exists_paired_all (Abs (_, _, t)) = exists_paired_all t
       | exists_paired_all _ = false;
     val ss = HOL_basic_ss
-      addsimps [thm "split_paired_all", thm "unit_all_eq2", thm "unit_abs_eta_conv"]
+      addsimps [@{thm split_paired_all}, @{thm unit_all_eq2}, @{thm unit_abs_eta_conv}]
       addsimprocs [unit_eq_proc];
   in
     val split_all_tac = SUBGOAL (fn (t, i) =>
@@ -340,10 +340,12 @@
     val unsafe_split_all_tac = SUBGOAL (fn (t, i) =>
       if exists_paired_all t then full_simp_tac ss i else no_tac);
     fun split_all th =
-   if exists_paired_all (#prop (Thm.rep_thm th)) then full_simplify ss th else th;
+   if exists_paired_all (Thm.prop_of th) then full_simplify ss th else th;
   end;
+*}
 
-change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac));
+declaration {* fn _ =>
+  Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))
 *}
 
 lemma split_paired_All [simp]: "(ALL x. P x) = (ALL a b. P (a, b))"
@@ -541,7 +543,7 @@
 declare mem_splitI2 [intro!] mem_splitI [intro!] splitI2' [intro!] splitI2 [intro!] splitI [intro!]
 declare mem_splitE [elim!] splitE' [elim!] splitE [elim!]
 
-ML_setup {*
+ML {*
 local (* filtering with exists_p_split is an essential optimization *)
   fun exists_p_split (Const ("split",_) $ _ $ (Const ("Pair",_)$_$_)) = true
     | exists_p_split (t $ u) = exists_p_split t orelse exists_p_split u
@@ -552,9 +554,12 @@
 val split_conv_tac = SUBGOAL (fn (t, i) =>
     if exists_p_split t then safe_full_simp_tac ss i else no_tac);
 end;
+*}
+
 (* This prevents applications of splitE for already splitted arguments leading
    to quite time-consuming computations (in particular for nested tuples) *)
-change_claset (fn cs => cs addSbefore ("split_conv_tac", split_conv_tac));
+declaration {* fn _ =>
+  Classical.map_cs (fn cs => cs addSbefore ("split_conv_tac", split_conv_tac))
 *}
 
 lemma split_eta_SetCompr [simp,noatp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
diff -r 7825c83c9eff -r a85fe32e7b2f src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Wed Mar 19 22:47:35 2008 +0100
+++ b/src/HOL/Transitive_Closure.thy	Wed Mar 19 22:47:38 2008 +0100
@@ -618,18 +618,18 @@
 
 subsection {* Setup of transitivity reasoner *}
 
-ML_setup {*
+ML {*
 
 structure Trancl_Tac = Trancl_Tac_Fun (
   struct
-    val r_into_trancl = thm "trancl.r_into_trancl";
-    val trancl_trans  = thm "trancl_trans";
-    val rtrancl_refl = thm "rtrancl.rtrancl_refl";
-    val r_into_rtrancl = thm "r_into_rtrancl";
-    val trancl_into_rtrancl = thm "trancl_into_rtrancl";
-    val rtrancl_trancl_trancl = thm "rtrancl_trancl_trancl";
-    val trancl_rtrancl_trancl = thm "trancl_rtrancl_trancl";
-    val rtrancl_trans = thm "rtrancl_trans";
+    val r_into_trancl = @{thm trancl.r_into_trancl};
+    val trancl_trans  = @{thm trancl_trans};
+    val rtrancl_refl = @{thm rtrancl.rtrancl_refl};
+    val r_into_rtrancl = @{thm r_into_rtrancl};
+    val trancl_into_rtrancl = @{thm trancl_into_rtrancl};
+    val rtrancl_trancl_trancl = @{thm rtrancl_trancl_trancl};
+    val trancl_rtrancl_trancl = @{thm trancl_rtrancl_trancl};
+    val rtrancl_trans = @{thm rtrancl_trans};
 
   fun decomp (Trueprop $ t) =
     let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) =
@@ -645,14 +645,14 @@
 
 structure Tranclp_Tac = Trancl_Tac_Fun (
   struct
-    val r_into_trancl = thm "tranclp.r_into_trancl";
-    val trancl_trans  = thm "tranclp_trans";
-    val rtrancl_refl = thm "rtranclp.rtrancl_refl";
-    val r_into_rtrancl = thm "r_into_rtranclp";
-    val trancl_into_rtrancl = thm "tranclp_into_rtranclp";
-    val rtrancl_trancl_trancl = thm "rtranclp_tranclp_tranclp";
-    val trancl_rtrancl_trancl = thm "tranclp_rtranclp_tranclp";
-    val rtrancl_trans = thm "rtranclp_trans";
+    val r_into_trancl = @{thm tranclp.r_into_trancl};
+    val trancl_trans  = @{thm tranclp_trans};
+    val rtrancl_refl = @{thm rtranclp.rtrancl_refl};
+    val r_into_rtrancl = @{thm r_into_rtranclp};
+    val trancl_into_rtrancl = @{thm tranclp_into_rtranclp};
+    val rtrancl_trancl_trancl = @{thm rtranclp_tranclp_tranclp};
+    val trancl_rtrancl_trancl = @{thm tranclp_rtranclp_tranclp};
+    val rtrancl_trans = @{thm rtranclp_trans};
 
   fun decomp (Trueprop $ t) =
     let fun dec (rel $ a $ b) =
@@ -665,13 +665,14 @@
     in dec t end;
 
   end);
+*}
 
-change_simpset (fn ss => ss
-  addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac))
-  addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac))
-  addSolver (mk_solver "Tranclp" (fn _ => Tranclp_Tac.trancl_tac))
-  addSolver (mk_solver "Rtranclp" (fn _ => Tranclp_Tac.rtrancl_tac)));
-
+declaration {* fn _ =>
+  Simplifier.map_ss (fn ss => ss
+    addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac))
+    addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac))
+    addSolver (mk_solver "Tranclp" (fn _ => Tranclp_Tac.trancl_tac))
+    addSolver (mk_solver "Rtranclp" (fn _ => Tranclp_Tac.rtrancl_tac)))
 *}
 
 (* Optional methods *)