--- a/src/HOL/Tools/inductive_realizer.ML Thu Nov 16 01:07:23 2006 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Thu Nov 16 01:07:25 2006 +0100
@@ -295,7 +295,7 @@
val (_ $ (_ $ _ $ S)) = Logic.strip_imp_concl (prop_of (hd intrs));
val (_, params) = strip_comb S;
val params' = map dest_Var params;
- val rss = [] |> Library.fold add_rule intrs;
+ val rss = [] |> fold add_rule intrs;
val (prfx, _) = split_last (NameSpace.unpack (fst (hd rss)));
val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;