src/HOL/Nominal/nominal_inductive.ML
changeset 38558 32ad17fe2b9c
parent 38549 d0385f2764d8
child 38715 6513ea67d95d
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Thu Aug 19 16:08:54 2010 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Aug 19 16:08:59 2010 +0200
     1.3 @@ -78,7 +78,7 @@
     1.4    | split_conj _ _ _ _ = NONE;
     1.5  
     1.6  fun strip_all [] t = t
     1.7 -  | strip_all (_ :: xs) (Const (@{const_name "All"}, _) $ Abs (s, T, t)) = strip_all xs t;
     1.8 +  | strip_all (_ :: xs) (Const (@{const_name All}, _) $ Abs (s, T, t)) = strip_all xs t;
     1.9  
    1.10  (*********************************************************************)
    1.11  (* maps  R ... & (ALL pi_1 ... pi_n z. P z (pi_1 o ... o pi_n o t))  *)