# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260437765 -3600
# Node ID 2779da3cd02cfeb405f7e8f78e842d0de886af0e
# Parent  af118149ffd4cc03535ee83f8675b0d277980f19
minor

diff -r af118149ffd4 -r 2779da3cd02c Quot/QuotMain.thy
--- 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