src/HOL/Modelcheck/mucke_oracle.ML
changeset 16587 b34c8aa657a5
parent 16486 1a12cdb6ee6b
child 17272 c63e5220ed77
     1.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Tue Jun 28 15:26:45 2005 +0200
     1.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Tue Jun 28 15:27:45 2005 +0200
     1.3 @@ -41,7 +41,7 @@
     1.4  local
     1.5    (* searching an if-term as below as possible *)
     1.6    fun contains_if (Abs(a,T,t)) = [] |
     1.7 -  contains_if (Const("If",T) $ b $ a1 $ a2) =
     1.8 +  contains_if (Const("HOL.If",T) $ b $ a1 $ a2) =
     1.9    let
    1.10    fun tn (Type(s,_)) = s |
    1.11    tn _ = error "cannot master type variables in if term";
    1.12 @@ -60,7 +60,7 @@
    1.13    find_replace_term t = (t,[]);
    1.14  
    1.15    fun if_substi (Abs(a,T,t)) trm = Abs(a,T,t) |
    1.16 -  if_substi (Const("If",T) $ b $ a1 $ a2) t = t |
    1.17 +  if_substi (Const("HOL.If",T) $ b $ a1 $ a2) t = t |
    1.18    if_substi (a $ b) t = if ((contains_if b)=[]) then ((if_substi a t)$b)
    1.19  		        else (a$(if_substi b t)) |
    1.20    if_substi t v = t;
    1.21 @@ -654,7 +654,7 @@
    1.22    val tty = type_of_term t;
    1.23    val con_term = con_term_of con a;
    1.24   in
    1.25 -	(Const("If",Type("fun",[Type("bool",[]),
    1.26 +	(Const("HOL.If",Type("fun",[Type("bool",[]),
    1.27          Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])])) $
    1.28  	(Const("op =",Type("fun",[tty,Type("fun",[tty,Type("bool",[])])])) $
    1.29          t $ con_term) $
    1.30 @@ -757,7 +757,7 @@
    1.31   fun casc_if2 sg tl x con [] ty trm [] = trm | (* should never occur *)
    1.32   casc_if2 sg tl x con [arg] ty trm [] = x_subst sg tl x (con_term_of con arg) trm |
    1.33   casc_if2 sg tl x con (a::r) ty trm cl =
    1.34 -        Const("If",Type("fun",[Type("bool",[]),
    1.35 +        Const("HOL.If",Type("fun",[Type("bool",[]),
    1.36          Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])
    1.37          ])) $
    1.38       (Const("op =",Type("fun",[ty,Type("fun",[ty,Type("bool",[])])])) $