src/Pure/Isar/code.ML
changeset 24283 8ca96f4e49cd
parent 24219 e558fe311376
child 24423 ae9cd0e92423
     1.1 --- a/src/Pure/Isar/code.ML	Wed Aug 15 08:57:41 2007 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Wed Aug 15 08:57:42 2007 +0200
     1.3 @@ -638,10 +638,8 @@
     1.4          | NONE => check_typ_fun (const, thm);
     1.5    in check_typ (fst (CodeUnit.head_func thm), thm) end;
     1.6  
     1.7 -val mk_func = CodeUnit.error_thm
     1.8 -  (assert_func_typ o CodeUnit.mk_func);
     1.9 -val mk_func_liberal = CodeUnit.warning_thm
    1.10 -  (assert_func_typ o CodeUnit.mk_func);
    1.11 +val mk_func = CodeUnit.error_thm (assert_func_typ o CodeUnit.mk_func);
    1.12 +val mk_func_liberal = CodeUnit.warning_thm (assert_func_typ o CodeUnit.mk_func);
    1.13  
    1.14  end;
    1.15