src/HOL/Transitive_Closure.thy

--- a/src/HOL/Transitive_Closure.thy	Sun Jul 26 22:24:13 2009 +0200
+++ b/src/HOL/Transitive_Closure.thy	Sun Jul 26 22:28:31 2009 +0200
@@ -811,16 +811,16 @@
 
 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};
+structure Trancl_Tac = Trancl_Tac
+(
+  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 (@{const Trueprop} $ t) =
     let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) =
@@ -832,19 +832,18 @@
       | dec _ =  NONE
     in dec t end
     | decomp _ = NONE;
-
-  end);
+);
 
-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};
+structure Tranclp_Tac = Trancl_Tac
+(
+  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 (@{const Trueprop} $ t) =
     let fun dec (rel $ a $ b) =
@@ -856,31 +855,31 @@
       | dec _ =  NONE
     in dec t end
     | decomp _ = NONE;
-
-  end);
+);
 *}
 
 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)))
+    addSolver (mk_solver' "Trancl" (Trancl_Tac.trancl_tac o Simplifier.the_context))
+    addSolver (mk_solver' "Rtrancl" (Trancl_Tac.rtrancl_tac o Simplifier.the_context))
+    addSolver (mk_solver' "Tranclp" (Tranclp_Tac.trancl_tac o Simplifier.the_context))
+    addSolver (mk_solver' "Rtranclp" (Tranclp_Tac.rtrancl_tac o Simplifier.the_context)))
 *}
 
-(* Optional methods *)
+
+text {* Optional methods. *}
 
 method_setup trancl =
-  {* Scan.succeed (K (SIMPLE_METHOD' Trancl_Tac.trancl_tac)) *}
+  {* Scan.succeed (SIMPLE_METHOD' o Trancl_Tac.trancl_tac) *}
   {* simple transitivity reasoner *}
 method_setup rtrancl =
-  {* Scan.succeed (K (SIMPLE_METHOD' Trancl_Tac.rtrancl_tac)) *}
+  {* Scan.succeed (SIMPLE_METHOD' o Trancl_Tac.rtrancl_tac) *}
   {* simple transitivity reasoner *}
 method_setup tranclp =
-  {* Scan.succeed (K (SIMPLE_METHOD' Tranclp_Tac.trancl_tac)) *}
+  {* Scan.succeed (SIMPLE_METHOD' o Tranclp_Tac.trancl_tac) *}
   {* simple transitivity reasoner (predicate version) *}
 method_setup rtranclp =
-  {* Scan.succeed (K (SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac)) *}
+  {* Scan.succeed (SIMPLE_METHOD' o Tranclp_Tac.rtrancl_tac) *}
   {* simple transitivity reasoner (predicate version) *}
 
 end