# HG changeset patch
# User haftmann
# Date 1499708938 -7200
# Node ID d6053815df065958f4b913cd354299d5eb83f0d1
# Parent  b5279a21e658a67c3c303f2392f056e5890e4228
tuned

diff -r b5279a21e658 -r d6053815df06 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;