src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
changeset 56245 84fc7dfa3cd4
parent 55966 972f0aa7091b
child 56765 644f0d4820a1
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -46,7 +46,7 @@
     1.4  
     1.5  fun hhf_concl_conv cv ctxt ct =
     1.6    (case Thm.term_of ct of
     1.7 -    Const (@{const_name all}, _) $ Abs _ =>
     1.8 +    Const (@{const_name Pure.all}, _) $ Abs _ =>
     1.9      Conv.arg_conv (Conv.abs_conv (hhf_concl_conv cv o snd) ctxt) ct
    1.10    | _ => Conv.concl_conv ~1 cv ct);
    1.11