src/HOL/Nominal/nominal_inductive.ML
changeset 38549 d0385f2764d8
parent 36960 01594f816e3a
child 38558 32ad17fe2b9c
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Thu Aug 19 10:27:12 2010 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Aug 19 11:02:14 2010 +0200
     1.3 @@ -71,14 +71,14 @@
     1.4    | add_binders thy i (Abs (_, _, t)) bs = add_binders thy (i + 1) t bs
     1.5    | add_binders thy i _ bs = bs;
     1.6  
     1.7 -fun split_conj f names (Const ("op &", _) $ p $ q) _ = (case head_of p of
     1.8 +fun split_conj f names (Const (@{const_name "op &"}, _) $ p $ q) _ = (case head_of p of
     1.9        Const (name, _) =>
    1.10          if member (op =) names name then SOME (f p q) else NONE
    1.11      | _ => NONE)
    1.12    | split_conj _ _ _ _ = NONE;
    1.13  
    1.14  fun strip_all [] t = t
    1.15 -  | strip_all (_ :: xs) (Const ("All", _) $ Abs (s, T, t)) = strip_all xs t;
    1.16 +  | strip_all (_ :: xs) (Const (@{const_name "All"}, _) $ Abs (s, T, t)) = strip_all xs t;
    1.17  
    1.18  (*********************************************************************)
    1.19  (* maps  R ... & (ALL pi_1 ... pi_n z. P z (pi_1 o ... o pi_n o t))  *)
    1.20 @@ -89,7 +89,7 @@
    1.21  (* where "id" protects the subformula from simplification            *)
    1.22  (*********************************************************************)
    1.23  
    1.24 -fun inst_conj_all names ps pis (Const ("op &", _) $ p $ q) _ =
    1.25 +fun inst_conj_all names ps pis (Const (@{const_name "op &"}, _) $ p $ q) _ =
    1.26        (case head_of p of
    1.27           Const (name, _) =>
    1.28             if member (op =) names name then SOME (HOLogic.mk_conj (p,