src/HOL/Tools/old_primrec.ML
changeset 33368 b1cf34f1855c
parent 33338 de76079f973a
child 33832 cff42395c246
--- a/src/HOL/Tools/old_primrec.ML	Fri Oct 30 18:33:21 2009 +0100
+++ b/src/HOL/Tools/old_primrec.ML	Sun Nov 01 15:24:45 2009 +0100
@@ -237,8 +237,8 @@
     val params_of = these o AList.lookup (op =) (maps constrs_of rec_eqns);
   in
     induct
-    |> RuleCases.rename_params (map params_of (maps (map #1 o #3 o #2) descr))
-    |> RuleCases.save induct
+    |> Rule_Cases.rename_params (map params_of (maps (map #1 o #3 o #2) descr))
+    |> Rule_Cases.save induct
   end;
 
 local