src/HOL/Tools/recdef_package.ML
changeset 24927 48e08f37ce92
parent 24867 e5b55d7be9bb
child 26336 a0e2b706ce73
     1.1 --- a/src/HOL/Tools/recdef_package.ML	Tue Oct 09 17:10:34 2007 +0200
     1.2 +++ b/src/HOL/Tools/recdef_package.ML	Tue Oct 09 17:10:36 2007 +0200
     1.3 @@ -271,7 +271,7 @@
     1.4        error ("No termination condition #" ^ string_of_int i ^
     1.5          " in recdef definition of " ^ quote name);
     1.6    in
     1.7 -    Specification.theorem_i Thm.internalK NONE (K I) (bname, atts)
     1.8 +    Specification.theorem Thm.internalK NONE (K I) (bname, atts)
     1.9        [] (Element.Shows [(("", []), [(HOLogic.mk_Trueprop tc, [])])]) int lthy
    1.10    end;
    1.11