src/Pure/Isar/code.ML
changeset 66265 d6053815df06
parent 66251 cd935b7cb3fb
child 66313 e8d2862ec203
equal deleted inserted replaced
66264:b5279a21e658 66265:d6053815df06
   553       else error ("Type arguments do not satisfy sort constraints of abstype certificate.");
   553       else error ("Type arguments do not satisfy sort constraints of abstype certificate.");
   554   in (thm, tyco) end;
   554   in (thm, tyco) end;
   555 
   555 
   556 in
   556 in
   557 
   557 
   558 fun generic_assert_eqn strictness thy check_patterns thm_proper =
   558 fun generic_assert_eqn strictness thy check_patterns eqn =
   559   handle_strictness fst (raw_assert_eqn thy check_patterns) strictness thy thm_proper;
   559   handle_strictness fst (raw_assert_eqn thy check_patterns) strictness thy eqn;
   560 
   560 
   561 fun generic_assert_abs_eqn strictness thy check_patterns thm =
   561 fun generic_assert_abs_eqn strictness thy check_patterns thm =
   562   handle_strictness I (raw_assert_abs_eqn thy check_patterns) strictness thy thm;
   562   handle_strictness I (raw_assert_abs_eqn thy check_patterns) strictness thy thm;
   563 
   563 
   564 end;
   564 end;