src/HOL/arith_data.ML
changeset 5553 ae42b36a50c2
parent 5429 0833486c23ce
child 5591 fbb4e1ac234d
     1.1 --- a/src/HOL/arith_data.ML	Thu Sep 24 17:16:06 1998 +0200
     1.2 +++ b/src/HOL/arith_data.ML	Thu Sep 24 17:17:14 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_nocheck [] (cterm_of sg (mk_eqv (t, u)))
     1.8 +  mk_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)))));