src/HOL/Prolog/prolog.ML
changeset 55151 f331472f1027
parent 55143 04448228381d
child 56245 84fc7dfa3cd4
     1.1 --- a/src/HOL/Prolog/prolog.ML	Sat Jan 25 23:50:49 2014 +0100
     1.2 +++ b/src/HOL/Prolog/prolog.ML	Sun Jan 26 13:45:40 2014 +0100
     1.3 @@ -54,7 +54,7 @@
     1.4      fun at  thm = case concl_of thm of
     1.5        _$(Const(@{const_name All} ,_)$Abs(s,_,_))=>
     1.6          let val s' = if s="P" then "PP" else s
     1.7 -        in at(thm RS (read_instantiate ctxt [(("x", 0), s')] [s'] spec)) end
     1.8 +        in at(thm RS (Rule_Insts.read_instantiate ctxt [(("x", 0), s')] [s'] spec)) end
     1.9      | _$(Const(@{const_name HOL.conj},_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
    1.10      | _$(Const(@{const_name HOL.implies},_)$_$_)     => at(thm RS mp)
    1.11      | _                             => [thm]