src/HOL/Decision_Procs/Approximation.thy
changeset 52131 366fa32ee2a3
parent 52090 ff1ec795604b
child 52272 47d138cae708
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Fri May 24 16:42:57 2013 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Fri May 24 17:00:46 2013 +0200
     1.3 @@ -3411,7 +3411,7 @@
     1.4          (term_of_float_float_option_list o float_float_option_list_of_term) t
     1.5      | _ => bad t;
     1.6  
     1.7 -  val normalize = eval o Envir.beta_norm o Pattern.eta_long [];
     1.8 +  val normalize = eval o Envir.beta_norm o Envir.eta_long [];
     1.9  
    1.10  in Thm.cterm_of thy (Logic.mk_equals (t, normalize t)) end
    1.11  *}