src/HOL/ex/SVC_Oracle.thy
changeset 56245 84fc7dfa3cd4
parent 52131 366fa32ee2a3
child 56256 1e01c159e7d9
     1.1 --- a/src/HOL/ex/SVC_Oracle.thy	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -100,7 +100,7 @@
     1.4        | fm t = replace t
     1.5      (*entry point, and abstraction of a meta-formula*)
     1.6      fun mt ((c as Const(@{const_name Trueprop}, _)) $ p) = c $ (fm p)
     1.7 -      | mt ((c as Const("==>", _)) $ p $ q)  = c $ (mt p) $ (mt q)
     1.8 +      | mt ((c as Const(@{const_name Pure.imp}, _)) $ p $ q)  = c $ (mt p) $ (mt q)
     1.9        | mt t = fm t  (*it might be a formula*)
    1.10    in (Logic.list_all (params, mt body), !pairs) end;
    1.11