src/HOL/arith_data.ML
changeset 5316 7a8975451a89
parent 5303 22029546d109
child 5353 0526ade4a23b
     1.1 --- a/src/HOL/arith_data.ML	Thu Aug 13 18:07:56 1998 +0200
     1.2 +++ b/src/HOL/arith_data.ML	Thu Aug 13 18:14:26 1998 +0200
     1.3 @@ -56,7 +56,7 @@
     1.4  val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
     1.5  
     1.6  fun prove_conv expand_tac norm_tac sg (t, u) =
     1.7 -  meta_eq (prove_goalw_cterm [] (cterm_of sg (mk_eqv (t, u)))
     1.8 +  meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv (t, u)))
     1.9      (K [expand_tac, norm_tac]))
    1.10    handle ERROR => error ("The error(s) above occurred while trying to prove " ^
    1.11      (string_of_cterm (cterm_of sg (mk_eqv (t, u)))));