--- a/Quot/QuotMain.thy	Thu Dec 10 10:21:51 2009 +0100
+++ b/Quot/QuotMain.thy	Thu Dec 10 10:36:05 2009 +0100
@@ -843,10 +843,9 @@
 fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt)
 *}
 
-(* Since the patterns for the lhs are different; there are 3 different make-insts *)
+(* Since the patterns for the lhs are different; there are 2 different make-insts *)
 (* 1: does  ? \<rightarrow> id *)
-(* 2: does id \<rightarrow> ? *)
-(* 3: does  ? \<rightarrow> ? *)
+(* 2: does  ? \<rightarrow> non-id *)
 ML {*
 fun make_inst lhs t =
   let