src/HOL/Prolog/prolog.ML
changeset 55143 04448228381d
parent 52233 eb84dab7d4c1
child 55151 f331472f1027
     1.1 --- a/src/HOL/Prolog/prolog.ML	Sat Jan 25 21:52:04 2014 +0100
     1.2 +++ b/src/HOL/Prolog/prolog.ML	Sat Jan 25 22:06:07 2014 +0100
     1.3 @@ -49,14 +49,16 @@
     1.4  fun check_HOHH thm  = (if isD (concl_of thm) andalso forall isG (prems_of thm)
     1.5                          then thm else raise not_HOHH);
     1.6  
     1.7 -fun atomizeD ctxt thm = let
     1.8 +fun atomizeD ctxt thm =
     1.9 +  let
    1.10      fun at  thm = case concl_of thm of
    1.11 -      _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS
    1.12 -        (read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec))
    1.13 +      _$(Const(@{const_name All} ,_)$Abs(s,_,_))=>
    1.14 +        let val s' = if s="P" then "PP" else s
    1.15 +        in at(thm RS (read_instantiate ctxt [(("x", 0), s')] [s'] spec)) end
    1.16      | _$(Const(@{const_name HOL.conj},_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
    1.17      | _$(Const(@{const_name HOL.implies},_)$_$_)     => at(thm RS mp)
    1.18      | _                             => [thm]
    1.19 -in map zero_var_indexes (at thm) end;
    1.20 +  in map zero_var_indexes (at thm) end;
    1.21  
    1.22  val atomize_ss =
    1.23    (empty_simpset @{context} |> Simplifier.set_mksimps (mksimps mksimps_pairs))