src/HOL/Tools/inductive_realizer.ML
changeset 21395 f34ac19659ae
parent 21022 3634641f9405
child 21646 c07b5b0e8492
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Thu Nov 16 01:07:23 2006 +0100
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu Nov 16 01:07:25 2006 +0100
     1.3 @@ -295,7 +295,7 @@
     1.4      val (_ $ (_ $ _ $ S)) = Logic.strip_imp_concl (prop_of (hd intrs));
     1.5      val (_, params) = strip_comb S;
     1.6      val params' = map dest_Var params;
     1.7 -    val rss = [] |> Library.fold add_rule intrs;
     1.8 +    val rss = [] |> fold add_rule intrs;
     1.9      val (prfx, _) = split_last (NameSpace.unpack (fst (hd rss)));
    1.10      val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
    1.11