# HG changeset patch
# User urbanc
# Date 1134990596 -3600
# Node ID 318d2c2710401193a916c51a5bf15d03ad50050a
# Parent  a31e52a3e6efce5cc26ac8ca96aefd2e83560600
tuned one comment

diff -r a31e52a3e6ef -r 318d2c271040 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Mon Dec 19 12:08:16 2005 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML	Mon Dec 19 12:09:56 2005 +0100
@@ -380,8 +380,9 @@
       val pt_noptn_inst = thm "pt_noption_inst";   
       val pt_fun_inst   = thm "pt_fun_inst";     
 
-     (* for all atom-kind combinations <ak>/<ak'> show that  *)
-     (* every <ak> is an instance of pt_<ak'>                *)
+     (* for all atom-kind combinations <ak>/<ak'> show that        *)
+     (* every <ak> is an instance of pt_<ak'>; the proof for       *)
+     (* ak!=ak' is by definition; the case ak=ak' uses at_pt_inst. *)
      val thy13 = fold (fn ak_name => fn thy =>
 	fold (fn ak_name' => fn thy' =>
          let