--- 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
--- 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"},