diff -r 0477785525be -r 85f8d8a8c711 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Jan 06 16:45:19 2012 +0100
+++ b/src/HOL/List.thy	Fri Jan 06 17:44:42 2012 +0100
@@ -349,90 +349,91 @@
 mangled). In such cases it can be advisable to introduce separate
 definitions for the list comprehensions in question.  *}
 
-nonterminal lc_gen and lc_qual and lc_quals
+nonterminal lc_qual and lc_quals
 
 syntax
-"_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list"  ("[_ . __")
-"_lc_gen" :: "lc_gen \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ <- _")
-"_lc_test" :: "bool \<Rightarrow> lc_qual" ("_")
-(*"_lc_let" :: "letbinds => lc_qual"  ("let _")*)
-"_lc_end" :: "lc_quals" ("]")
-"_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals" (", __")
-"_lc_abs" :: "'a => 'b list => 'b list"
-"_strip_positions" :: "'a \<Rightarrow> lc_gen"  ("_")
+  "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list"  ("[_ . __")
+  "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  ("_ <- _")
+  "_lc_test" :: "bool \<Rightarrow> lc_qual" ("_")
+  (*"_lc_let" :: "letbinds => lc_qual"  ("let _")*)
+  "_lc_end" :: "lc_quals" ("]")
+  "_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals"  (", __")
+  "_lc_abs" :: "'a => 'b list => 'b list"
 
 (* These are easier than ML code but cannot express the optimized
    translation of [e. p<-xs]
 translations
-"[e. p<-xs]" => "concat(map (_lc_abs p [e]) xs)"
-"_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)"
- => "concat (map (_lc_abs p (_listcompr e Q Qs)) xs)"
-"[e. P]" => "if P then [e] else []"
-"_listcompr e (_lc_test P) (_lc_quals Q Qs)"
- => "if P then (_listcompr e Q Qs) else []"
-"_listcompr e (_lc_let b) (_lc_quals Q Qs)"
- => "_Let b (_listcompr e Q Qs)"
+  "[e. p<-xs]" => "concat(map (_lc_abs p [e]) xs)"
+  "_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)"
+   => "concat (map (_lc_abs p (_listcompr e Q Qs)) xs)"
+  "[e. P]" => "if P then [e] else []"
+  "_listcompr e (_lc_test P) (_lc_quals Q Qs)"
+   => "if P then (_listcompr e Q Qs) else []"
+  "_listcompr e (_lc_let b) (_lc_quals Q Qs)"
+   => "_Let b (_listcompr e Q Qs)"
 *)
 
 syntax (xsymbols)
-"_lc_gen" :: "lc_gen \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
+  "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  ("_ \<leftarrow> _")
 syntax (HTML output)
-"_lc_gen" :: "lc_gen \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
+  "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  ("_ \<leftarrow> _")
 
 parse_translation (advanced) {*
-let
-  val NilC = Syntax.const @{const_syntax Nil};
-  val ConsC = Syntax.const @{const_syntax Cons};
-  val mapC = Syntax.const @{const_syntax map};
-  val concatC = Syntax.const @{const_syntax concat};
-  val IfC = Syntax.const @{const_syntax If};
-
-  fun singl x = ConsC $ x $ NilC;
-
-  fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
-    let
-      (* FIXME proper name context!? *)
-      val x = Free (singleton (Name.variant_list (fold Term.add_free_names [p, e] [])) "x", dummyT);
-      val e = if opti then singl e else e;
-      val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e;
-      val case2 =
-        Syntax.const @{syntax_const "_case1"} $
-          Syntax.const @{const_syntax dummy_pattern} $ NilC;
-      val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2;
-      val ft = Datatype_Case.case_tr false ctxt [x, cs];
-    in lambda x ft end;
-
-  fun abs_tr ctxt (p as Free (s, T)) e opti =
-        let
-          val thy = Proof_Context.theory_of ctxt;
-          val s' = Proof_Context.intern_const ctxt s;
-        in
-          if Sign.declared_const thy s'
-          then (pat_tr ctxt p e opti, false)
-          else (lambda p e, true)
-        end
-    | abs_tr ctxt p e opti = (pat_tr ctxt p e opti, false);
-
-  fun lc_tr ctxt [e, Const (@{syntax_const "_lc_test"}, _) $ b, qs] =
-        let
-          val res =
-            (case qs of
-              Const (@{syntax_const "_lc_end"}, _) => singl e
-            | Const (@{syntax_const "_lc_quals"}, _) $ q $ qs => lc_tr ctxt [e, q, qs]);
-        in IfC $ b $ res $ NilC end
-    | lc_tr ctxt
-          [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,
-            Const(@{syntax_const "_lc_end"}, _)] =
-        (case abs_tr ctxt p e true of
-          (f, true) => mapC $ f $ es
-        | (f, false) => concatC $ (mapC $ f $ es))
-    | lc_tr ctxt
-          [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,
-            Const (@{syntax_const "_lc_quals"}, _) $ q $ qs] =
-        let val e' = lc_tr ctxt [e, q, qs];
-        in concatC $ (mapC $ (fst (abs_tr ctxt p e' false)) $ es) end;
-
-in [(@{syntax_const "_listcompr"}, lc_tr)] end
+  let
+    val NilC = Syntax.const @{const_syntax Nil};
+    val ConsC = Syntax.const @{const_syntax Cons};
+    val mapC = Syntax.const @{const_syntax map};
+    val concatC = Syntax.const @{const_syntax concat};
+    val IfC = Syntax.const @{const_syntax If};
+
+    fun single x = ConsC $ x $ NilC;
+
+    fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
+      let
+        (* FIXME proper name context!? *)
+        val x =
+          Free (singleton (Name.variant_list (fold Term.add_free_names [p, e] [])) "x", dummyT);
+        val e = if opti then single e else e;
+        val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e;
+        val case2 =
+          Syntax.const @{syntax_const "_case1"} $
+            Syntax.const @{const_syntax dummy_pattern} $ NilC;
+        val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2;
+      in Syntax_Trans.abs_tr [x, Datatype_Case.case_tr false ctxt [x, cs]] end;
+
+    fun abs_tr ctxt p e opti =
+      (case Term_Position.strip_positions p of
+        Free (s, T) =>
+          let
+            val thy = Proof_Context.theory_of ctxt;
+            val s' = Proof_Context.intern_const ctxt s;
+          in
+            if Sign.declared_const thy s'
+            then (pat_tr ctxt p e opti, false)
+            else (Syntax_Trans.abs_tr [p, e], true)
+          end
+      | _ => (pat_tr ctxt p e opti, false));
+
+    fun lc_tr ctxt [e, Const (@{syntax_const "_lc_test"}, _) $ b, qs] =
+          let
+            val res =
+              (case qs of
+                Const (@{syntax_const "_lc_end"}, _) => single e
+              | Const (@{syntax_const "_lc_quals"}, _) $ q $ qs => lc_tr ctxt [e, q, qs]);
+          in IfC $ b $ res $ NilC end
+      | lc_tr ctxt
+            [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,
+              Const(@{syntax_const "_lc_end"}, _)] =
+          (case abs_tr ctxt p e true of
+            (f, true) => mapC $ f $ es
+          | (f, false) => concatC $ (mapC $ f $ es))
+      | lc_tr ctxt
+            [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,
+              Const (@{syntax_const "_lc_quals"}, _) $ q $ qs] =
+          let val e' = lc_tr ctxt [e, q, qs];
+          in concatC $ (mapC $ (fst (abs_tr ctxt p e' false)) $ es) end;
+
+  in [(@{syntax_const "_listcompr"}, lc_tr)] end
 *}
 
 ML {*