diff -r 11140987d415 -r ef1ddc59b825 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Jun 29 16:31:50 2011 +0200
+++ b/src/HOL/List.thy	Wed Jun 29 17:35:46 2011 +0200
@@ -726,54 +726,44 @@
 - or both lists end in the same list.
 *}
 
-ML {*
-local
-
-fun last (cons as Const(@{const_name Cons},_) $ _ $ xs) =
-  (case xs of Const(@{const_name Nil},_) => cons | _ => last xs)
-  | last (Const(@{const_name append},_) $ _ $ ys) = last ys
-  | last t = t;
-
-fun list1 (Const(@{const_name Cons},_) $ _ $ Const(@{const_name Nil},_)) = true
-  | list1 _ = false;
-
-fun butlast ((cons as Const(@{const_name Cons},_) $ x) $ xs) =
-  (case xs of Const(@{const_name Nil},_) => xs | _ => cons $ butlast xs)
-  | butlast ((app as Const(@{const_name append},_) $ xs) $ ys) = app $ butlast ys
-  | butlast xs = Const(@{const_name Nil},fastype_of xs);
-
-val rearr_ss = HOL_basic_ss addsimps [@{thm append_assoc},
-  @{thm append_Nil}, @{thm append_Cons}];
-
-fun list_eq ss (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
+simproc_setup list_eq ("(xs::'a list) = ys")  = {*
   let
-    val lastl = last lhs and lastr = last rhs;
-    fun rearr conv =
+    fun last (cons as Const (@{const_name Cons}, _) $ _ $ xs) =
+          (case xs of Const (@{const_name Nil}, _) => cons | _ => last xs)
+      | last (Const(@{const_name append},_) $ _ $ ys) = last ys
+      | last t = t;
+    
+    fun list1 (Const(@{const_name Cons},_) $ _ $ Const(@{const_name Nil},_)) = true
+      | list1 _ = false;
+    
+    fun butlast ((cons as Const(@{const_name Cons},_) $ x) $ xs) =
+          (case xs of Const (@{const_name Nil}, _) => xs | _ => cons $ butlast xs)
+      | butlast ((app as Const (@{const_name append}, _) $ xs) $ ys) = app $ butlast ys
+      | butlast xs = Const(@{const_name Nil}, fastype_of xs);
+    
+    val rearr_ss =
+      HOL_basic_ss addsimps [@{thm append_assoc}, @{thm append_Nil}, @{thm append_Cons}];
+    
+    fun list_eq ss (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
       let
-        val lhs1 = butlast lhs and rhs1 = butlast rhs;
-        val Type(_,listT::_) = eqT
-        val appT = [listT,listT] ---> listT
-        val app = Const(@{const_name append},appT)
-        val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
-        val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));
-        val thm = Goal.prove (Simplifier.the_context ss) [] [] eq
-          (K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1));
-      in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;
-
-  in
-    if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv}
-    else if lastl aconv lastr then rearr @{thm append_same_eq}
-    else NONE
-  end;
-
-in
-
-val list_eq_simproc =
-  Simplifier.simproc_global @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq);
-
-end;
-
-Addsimprocs [list_eq_simproc];
+        val lastl = last lhs and lastr = last rhs;
+        fun rearr conv =
+          let
+            val lhs1 = butlast lhs and rhs1 = butlast rhs;
+            val Type(_,listT::_) = eqT
+            val appT = [listT,listT] ---> listT
+            val app = Const(@{const_name append},appT)
+            val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
+            val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));
+            val thm = Goal.prove (Simplifier.the_context ss) [] [] eq
+              (K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1));
+          in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;
+      in
+        if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv}
+        else if lastl aconv lastr then rearr @{thm append_same_eq}
+        else NONE
+      end;
+  in fn _ => fn ss => fn ct => list_eq ss (term_of ct) end;
 *}