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