changeset 12004 | 1703de633aaf |
parent 11740 | 86ac4189a1c1 |
child 12043 | 8c86683597a8 |
--- a/src/HOL/Tools/recdef_package.ML Wed Oct 31 21:58:04 2001 +0100 +++ b/src/HOL/Tools/recdef_package.ML Wed Oct 31 21:59:07 2001 +0100 @@ -310,7 +310,7 @@ error ("No termination condition #" ^ string_of_int i ^ " in recdef definition of " ^ quote name); in - thy |> IsarThy.theorem_i Drule.internalK + thy |> IsarThy.theorem_i Drule.internalK None (((bname, atts), (HOLogic.mk_Trueprop tc, ([], []))), Comment.none) int end;