src/HOL/Tools/recdef_package.ML
changeset 7262 a05dc63ca29b
parent 6851 526c0b90bcef
child 7798 42e94b618f34
     1.1 --- a/src/HOL/Tools/recdef_package.ML	Wed Aug 18 18:10:48 1999 +0200
     1.2 +++ b/src/HOL/Tools/recdef_package.ML	Wed Aug 18 18:44:20 1999 +0200
     1.3 @@ -85,8 +85,8 @@
     1.4  
     1.5      val ss = (case raw_ss of None => Simplifier.simpset_of thy | Some x => prep_ss x);
     1.6      val (thy1, congs) = thy |> app_thms raw_congs;
     1.7 -    val (thy2, pats) = tfl_fn thy1 name R eqs;
     1.8 -    val (result as {rules, induct, tcs}) = Tfl.simplify_defn (ss, congs) (thy2, (name, pats));
     1.9 +    val (thy2, result as {rules, induct, tcs}) = 
    1.10 +        tfl_fn thy1 name R (ss, congs) eqs
    1.11      val thy3 =
    1.12        thy2
    1.13        |> Theory.add_path bname