tuned
authorhaftmann
Mon, 10 Jul 2017 19:48:58 +0200
changeset 66265 d6053815df06
parent 66264 b5279a21e658
child 66266 130dea8500cb
tuned
src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sat Jul 08 20:05:26 2017 +0200
+++ b/src/Pure/Isar/code.ML	Mon Jul 10 19:48:58 2017 +0200
@@ -555,8 +555,8 @@
 
 in
 
-fun generic_assert_eqn strictness thy check_patterns thm_proper =
-  handle_strictness fst (raw_assert_eqn thy check_patterns) strictness thy thm_proper;
+fun generic_assert_eqn strictness thy check_patterns eqn =
+  handle_strictness fst (raw_assert_eqn thy check_patterns) strictness thy eqn;
 
 fun generic_assert_abs_eqn strictness thy check_patterns thm =
   handle_strictness I (raw_assert_abs_eqn thy check_patterns) strictness thy thm;