# HG changeset patch
# User haftmann
# Date 1178689988 -7200
# Node ID 2a3e9c7b894c1bc6816fffc32836b9ecbc1a774f
# Parent  cdff6ef76009ee348510a2dbc233327bf532f3aa
tuned

diff -r cdff6ef76009 -r 2a3e9c7b894c src/HOL/Tools/recfun_codegen.ML
--- a/src/HOL/Tools/recfun_codegen.ML	Wed May 09 07:53:06 2007 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML	Wed May 09 07:53:08 2007 +0200
@@ -72,7 +72,7 @@
      NONE => ([], "")
    | SOME thms => 
        let val thms' = del_redundant thy []
-         (List.filter (fn (thm, _) => is_instance thy T
+         (filter (fn (thm, _) => is_instance thy T
            (snd (const_of (prop_of thm)))) thms)
        in if null thms' then ([], "")
          else (preprocess thy (map fst thms'),
@@ -88,9 +88,9 @@
 
 exception EQN of string * typ * string;
 
-fun cycle g (xs, x) =
-  if x mem xs then xs
-  else Library.foldl (cycle g) (x :: xs, List.concat (Graph.all_paths (fst g) (x, x)));
+fun cycle g (xs, x : string) =
+  if member (op =) xs x then xs
+  else Library.foldl (cycle g) (x :: xs, flat (Graph.all_paths (fst g) (x, x)));
 
 fun add_rec_funs thy defs gr dep eqs module =
   let
diff -r cdff6ef76009 -r 2a3e9c7b894c src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Wed May 09 07:53:06 2007 +0200
+++ b/src/HOL/arith_data.ML	Wed May 09 07:53:08 2007 +0200
@@ -926,8 +926,7 @@
     mult_mono_thms = mult_mono_thms,
     inj_thms = inj_thms,
     lessD = lessD @ [thm "Suc_leI"],
-    neqE = [@{thm linorder_neqE_nat},
-      get_thm (theory "Ring_and_Field") (Name "linorder_neqE_ordered_idom")],
+    neqE = [@{thm linorder_neqE_nat}, @{thm linorder_neqE_ordered_idom}],
     simpset = HOL_basic_ss
       addsimps [@{thm "add_zero_left"}, @{thm "add_zero_right"},
         @{thm "Zero_not_Suc"}, @{thm "Suc_not_Zero"}, @{thm "le_0_eq"}, @{thm "One_nat_def"},