src/HOL/ex/SVC_Oracle.thy
changeset 46218 ecf6375e2abb
parent 44064 5bce8ff0d9ae
child 48891 c0eafbd55de3
     1.1 --- a/src/HOL/ex/SVC_Oracle.thy	Sat Jan 14 19:06:05 2012 +0100
     1.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Sat Jan 14 20:05:58 2012 +0100
     1.3 @@ -101,7 +101,7 @@
     1.4      fun mt ((c as Const(@{const_name Trueprop}, _)) $ p) = c $ (fm p)
     1.5        | mt ((c as Const("==>", _)) $ p $ q)  = c $ (mt p) $ (mt q)
     1.6        | mt t = fm t  (*it might be a formula*)
     1.7 -  in (list_all (params, mt body), !pairs) end;
     1.8 +  in (Logic.list_all (params, mt body), !pairs) end;
     1.9  
    1.10  
    1.11  (*Present the entire subgoal to the oracle, assumptions and all, but possibly