src/Pure/Isar/code.ML
changeset 24283 8ca96f4e49cd
parent 24219 e558fe311376
child 24423 ae9cd0e92423
--- a/src/Pure/Isar/code.ML	Wed Aug 15 08:57:41 2007 +0200
+++ b/src/Pure/Isar/code.ML	Wed Aug 15 08:57:42 2007 +0200
@@ -638,10 +638,8 @@
         | NONE => check_typ_fun (const, thm);
   in check_typ (fst (CodeUnit.head_func thm), thm) end;
 
-val mk_func = CodeUnit.error_thm
-  (assert_func_typ o CodeUnit.mk_func);
-val mk_func_liberal = CodeUnit.warning_thm
-  (assert_func_typ o CodeUnit.mk_func);
+val mk_func = CodeUnit.error_thm (assert_func_typ o CodeUnit.mk_func);
+val mk_func_liberal = CodeUnit.warning_thm (assert_func_typ o CodeUnit.mk_func);
 
 end;