src/HOL/arith_data.ML
changeset 5303 22029546d109
parent 5132 24f992a25adc
child 5316 7a8975451a89
     1.1 --- a/src/HOL/arith_data.ML	Wed Aug 12 16:16:49 1998 +0200
     1.2 +++ b/src/HOL/arith_data.ML	Wed Aug 12 16:20:49 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 -  mk_meta_eq (prove_goalw_cterm [] (cterm_of sg (mk_eqv (t, u)))
     1.8 +  meta_eq (prove_goalw_cterm [] (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)))));