src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
changeset 42568 7b9801a34836
parent 42563 e70ffe3846d0
child 42570 77f94ac04f32
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
     1.3 @@ -359,7 +359,7 @@
     1.4            end
     1.5          | SOME b =>
     1.6            let val (b, mangled_us) = b |> unmangled_const |>> invert_const in
     1.7 -            if b = boolify_base then
     1.8 +            if b = predicator_base then
     1.9                aux (SOME @{typ bool}) [] (hd us)
    1.10              else if b = explicit_app_base then
    1.11                aux opt_T (nth us 1 :: extra_us) (hd us)