--- a/src/HOL/Tools/recdef_package.ML Thu Mar 03 09:22:35 2005 +0100
+++ b/src/HOL/Tools/recdef_package.ML Thu Mar 03 12:43:01 2005 +0100
@@ -91,7 +91,7 @@
val (del, rest) = Library.partition (Library.equal c o fst) congs;
in if null del then (warning ("No recdef congruence rule for " ^ quote c); congs) else rest end;
-val add_congs = curry (foldr (uncurry add_cong));
+val add_congs = curry (Library.foldr (uncurry add_cong));
end;
@@ -255,7 +255,7 @@
val (thy, (simps' :: rules', [induct'])) =
thy
|> Theory.add_path bname
- |> PureThy.add_thmss ((("simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
+ |> PureThy.add_thmss ((("simps", List.concat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
|>>> PureThy.add_thms [(("induct", induct), [])];
val result = {simps = simps', rules = rules', induct = induct', tcs = tcs};
val thy =
@@ -312,8 +312,8 @@
(case get_recdef thy name of
NONE => error ("No recdef definition of constant: " ^ quote name)
| SOME {tcs, ...} => tcs);
- val i = if_none opt_i 1;
- val tc = Library.nth_elem (i - 1, tcs) handle Library.LIST _ =>
+ val i = getOpt (opt_i, 1);
+ val tc = List.nth (tcs, i - 1) handle Subscript =>
error ("No termination condition #" ^ string_of_int i ^
" in recdef definition of " ^ quote name);
in