src/HOL/Nominal/nominal_atoms.ML
changeset 30595 c87a3350f5a9
parent 30345 76fd85bbf139
child 31059 45c085c7efc6
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Thu Mar 19 21:05:40 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Thu Mar 19 22:05:00 2009 +0100
     1.3 @@ -106,8 +106,8 @@
     1.4                val ak_type = Type (Sign.intern_type thy1 ak,[])
     1.5                val ak_sign = Sign.intern_const thy1 ak 
     1.6                
     1.7 -              val inj_type = @{typ nat}-->ak_type
     1.8 -              val inj_on_type = inj_type-->(@{typ "nat set"})-->@{typ bool}  
     1.9 +              val inj_type = @{typ nat} --> ak_type
    1.10 +              val inj_on_type = inj_type --> @{typ "nat set"} --> @{typ bool}
    1.11  
    1.12                (* first statement *)
    1.13                val stmnt1 = HOLogic.mk_Trueprop