# HG changeset patch
# User haftmann
# Date 1246366472 -7200
# Node ID 3b08dcd74229cfaa77f8934e8136f7b9fa6981e6
# Parent  d262a0d4624653cc92a31b06e212ff9e95d5977c# Parent  f172346ba8056c21a4976f32bb454eca53dd8b34
merged

diff -r d262a0d46246 -r 3b08dcd74229 src/HOL/Imperative_HOL/Array.thy
--- a/src/HOL/Imperative_HOL/Array.thy	Tue Jun 30 11:21:02 2009 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy	Tue Jun 30 14:54:32 2009 +0200
@@ -1,5 +1,4 @@
-(*  Title:      HOL/Library/Array.thy
-    ID:         $Id$
+(*  Title:      HOL/Imperative_HOL/Array.thy
     Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
 *)
 
diff -r d262a0d46246 -r 3b08dcd74229 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jun 30 11:21:02 2009 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jun 30 14:54:32 2009 +0200
@@ -306,67 +306,75 @@
 code_const "Heap_Monad.Fail" (OCaml "Failure")
 code_const "Heap_Monad.raise_exc" (OCaml "!(fun/ ()/ ->/ raise/ _)")
 
-setup {* let
-  open Code_Thingol;
+setup {*
+
+let
 
-  fun lookup naming = the o Code_Thingol.lookup_const naming;
+open Code_Thingol;
+
+fun imp_program naming =
 
-  fun imp_monad_bind'' bind' return' unit' ts =
-    let
-      val dummy_name = "";
-      val dummy_type = ITyVar dummy_name;
-      val dummy_case_term = IVar dummy_name;
-      (*assumption: dummy values are not relevant for serialization*)
-      val unitt = IConst (unit', (([], []), []));
-      fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
-        | dest_abs (t, ty) =
-            let
-              val vs = Code_Thingol.fold_varnames cons t [];
-              val v = Name.variant vs "x";
-              val ty' = (hd o fst o Code_Thingol.unfold_fun) ty;
-            in ((v, ty'), t `$ IVar v) end;
-      fun force (t as IConst (c, _) `$ t') = if c = return'
-            then t' else t `$ unitt
-        | force t = t `$ unitt;
-      fun tr_bind' [(t1, _), (t2, ty2)] =
-        let
-          val ((v, ty), t) = dest_abs (t2, ty2);
-        in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end
-      and tr_bind'' t = case Code_Thingol.unfold_app t
-           of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if c = bind'
-                then tr_bind' [(x1, ty1), (x2, ty2)]
-                else force t
-            | _ => force t;
-    in (dummy_name, dummy_type) `|=> ICase (((IVar dummy_name, dummy_type),
-      [(unitt, tr_bind' ts)]), dummy_case_term) end
-  and imp_monad_bind' bind' return' unit' (const as (c, (_, tys))) ts = if c = bind' then case (ts, tys)
-     of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' bind' return' unit' [(t1, ty1), (t2, ty2)]
-      | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' bind' return' unit' [(t1, ty1), (t2, ty2)] `$ t3
-      | (ts, _) => imp_monad_bind bind' return' unit' (eta_expand 2 (const, ts))
-    else IConst const `$$ map (imp_monad_bind bind' return' unit') ts
-  and imp_monad_bind bind' return' unit' (IConst const) = imp_monad_bind' bind' return' unit' const []
-    | imp_monad_bind bind' return' unit' (t as IVar _) = t
-    | imp_monad_bind bind' return' unit' (t as _ `$ _) = (case unfold_app t
-       of (IConst const, ts) => imp_monad_bind' bind' return' unit' const ts
-        | (t, ts) => imp_monad_bind bind' return' unit' t `$$ map (imp_monad_bind bind' return' unit') ts)
-    | imp_monad_bind bind' return' unit' (v_ty `|=> t) = v_ty `|=> imp_monad_bind bind' return' unit' t
-    | imp_monad_bind bind' return' unit' (ICase (((t, ty), pats), t0)) = ICase
-        (((imp_monad_bind bind' return' unit' t, ty), (map o pairself) (imp_monad_bind bind' return' unit') pats), imp_monad_bind bind' return' unit' t0);
+  let
+    fun is_const c = case lookup_const naming c
+     of SOME c' => (fn c'' => c' = c'')
+      | NONE => K false;
+    val is_bindM = is_const @{const_name bindM};
+    val is_return = is_const @{const_name return};
+    val dummy_name = "X";
+    val dummy_type = ITyVar dummy_name;
+    val dummy_case_term = IVar "";
+    (*assumption: dummy values are not relevant for serialization*)
+    val unitt = case lookup_const naming @{const_name Unity}
+     of SOME unit' => IConst (unit', (([], []), []))
+      | NONE => error ("Must include " ^ @{const_name Unity} ^ " in generated constants.");
+    fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
+      | dest_abs (t, ty) =
+          let
+            val vs = fold_varnames cons t [];
+            val v = Name.variant vs "x";
+            val ty' = (hd o fst o unfold_fun) ty;
+          in ((v, ty'), t `$ IVar v) end;
+    fun force (t as IConst (c, _) `$ t') = if is_return c
+          then t' else t `$ unitt
+      | force t = t `$ unitt;
+    fun tr_bind' [(t1, _), (t2, ty2)] =
+      let
+        val ((v, ty), t) = dest_abs (t2, ty2);
+      in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end
+    and tr_bind'' t = case unfold_app t
+         of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if is_bindM c
+              then tr_bind' [(x1, ty1), (x2, ty2)]
+              else force t
+          | _ => force t;
+    fun imp_monad_bind'' ts = (dummy_name, dummy_type) `|=> ICase (((IVar dummy_name, dummy_type),
+      [(unitt, tr_bind' ts)]), dummy_case_term)
+    and imp_monad_bind' (const as (c, (_, tys))) ts = if is_bindM c then case (ts, tys)
+       of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)]
+        | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3
+        | (ts, _) => imp_monad_bind (eta_expand 2 (const, ts))
+      else IConst const `$$ map imp_monad_bind ts
+    and imp_monad_bind (IConst const) = imp_monad_bind' const []
+      | imp_monad_bind (t as IVar _) = t
+      | imp_monad_bind (t as _ `$ _) = (case unfold_app t
+         of (IConst const, ts) => imp_monad_bind' const ts
+          | (t, ts) => imp_monad_bind t `$$ map imp_monad_bind ts)
+      | imp_monad_bind (v_ty `|=> t) = v_ty `|=> imp_monad_bind t
+      | imp_monad_bind (ICase (((t, ty), pats), t0)) = ICase
+          (((imp_monad_bind t, ty),
+            (map o pairself) imp_monad_bind pats),
+              imp_monad_bind t0);
 
-  fun imp_program naming = (Graph.map_nodes o map_terms_stmt)
-    (imp_monad_bind (lookup naming @{const_name bindM})
-      (lookup naming @{const_name return})
-      (lookup naming @{const_name Unity}));
+  in (Graph.map_nodes o map_terms_stmt) imp_monad_bind end;
 
 in
 
-  Code_Target.extend_target ("SML_imp", ("SML", imp_program))
-  #> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program))
+Code_Target.extend_target ("SML_imp", ("SML", imp_program))
+#> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program))
 
 end
+
 *}
 
-
 code_reserved OCaml Failure raise
 
 
diff -r d262a0d46246 -r 3b08dcd74229 src/HOL/Imperative_HOL/Imperative_HOL_ex.thy
--- a/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Tue Jun 30 11:21:02 2009 +0200
+++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Tue Jun 30 14:54:32 2009 +0200
@@ -1,8 +1,9 @@
 (*  Title:      HOL/Imperative_HOL/Imperative_HOL_ex.thy
-    Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
+    Author:     John Matthews, Galois Connections;
+                Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
 *)
 
-header {* Mmonadic imperative HOL with examples *}
+header {* Monadic imperative HOL with examples *}
 
 theory Imperative_HOL_ex
 imports Imperative_HOL "ex/Imperative_Quicksort"
diff -r d262a0d46246 -r 3b08dcd74229 src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Jun 30 11:21:02 2009 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Jun 30 14:54:32 2009 +0200
@@ -631,9 +631,9 @@
 
 ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *}
 
-export_code qsort in SML_imp module_name QSort
+(*export_code qsort in SML_imp module_name QSort*)
 export_code qsort in OCaml module_name QSort file -
-export_code qsort in OCaml_imp module_name QSort file -
+(*export_code qsort in OCaml_imp module_name QSort file -*)
 export_code qsort in Haskell module_name QSort file -
 
 end
\ No newline at end of file
diff -r d262a0d46246 -r 3b08dcd74229 src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Tue Jun 30 11:21:02 2009 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Tue Jun 30 14:54:32 2009 +0200
@@ -450,7 +450,7 @@
 qed
 
 lemma [code]:
-  "iter f step ss w = while (\<lambda>(ss, w). \<not> (is_empty w))
+  "iter f step ss w = while (\<lambda>(ss, w). \<not> is_empty w)
     (\<lambda>(ss, w).
         let p = some_elem w in propa f (step p (ss ! p)) ss (w - {p}))
     (ss, w)"
diff -r d262a0d46246 -r 3b08dcd74229 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Tue Jun 30 11:21:02 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Tue Jun 30 14:54:32 2009 +0200
@@ -18,7 +18,7 @@
   val the_info : theory -> string -> info
   val the_descr : theory -> string list
     -> descr * (string * sort) list * string list
-      * (string list * string list) * (typ list * typ list)
+      * string * (string list * string list) * (typ list * typ list)
   val the_spec : theory -> string -> (string * sort) list * (string * typ list) list
   val get_constrs : theory -> string -> (string * typ) list option
   val get_all : theory -> info Symtab.table
@@ -125,9 +125,10 @@
 
     val names = map Long_Name.base_name (the_default tycos (#alt_names info));
     val (auxnames, _) = Name.make_context names
-      |> fold_map (yield_singleton Name.variants o name_of_typ) Us
+      |> fold_map (yield_singleton Name.variants o name_of_typ) Us;
+    val prefix = space_implode "_" names;
 
-  in (descr, vs, tycos, (names, auxnames), (Ts, Us)) end;
+  in (descr, vs, tycos, prefix, (names, auxnames), (Ts, Us)) end;
 
 fun get_constrs thy dtco =
   case try (the_spec thy) dtco
diff -r d262a0d46246 -r 3b08dcd74229 src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Tue Jun 30 11:21:02 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Tue Jun 30 14:54:32 2009 +0200
@@ -11,10 +11,10 @@
     -> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
     -> seed -> (('a -> 'b) * (unit -> Term.term)) * seed
   val ensure_random_typecopy: string -> theory -> theory
-  val random_aux_specification: string -> term list -> local_theory -> local_theory
+  val random_aux_specification: string -> string -> term list -> local_theory -> local_theory
   val mk_random_aux_eqs: theory -> Datatype.descr -> (string * sort) list
     -> string list -> string list * string list -> typ list * typ list
-    -> string * (term list * (term * term) list)
+    -> term list * (term * term) list
   val ensure_random_datatype: Datatype.config -> string list -> theory -> theory
   val eval_ref: (unit -> int -> seed -> term list option * seed) option ref
   val setup: theory -> theory
@@ -184,18 +184,18 @@
 
 end;
 
-fun random_aux_primrec_multi prefix [eq] lthy =
+fun random_aux_primrec_multi auxname [eq] lthy =
       lthy
       |> random_aux_primrec eq
       |>> (fn simp => [simp])
-  | random_aux_primrec_multi prefix (eqs as _ :: _ :: _) lthy =
+  | random_aux_primrec_multi auxname (eqs as _ :: _ :: _) lthy =
       let
         val thy = ProofContext.theory_of lthy;
         val (lhss, rhss) = map_split (HOLogic.dest_eq o HOLogic.dest_Trueprop) eqs;
         val (vs, (arg as Free (v, _)) :: _) = map_split (fn (t1 $ t2) => (t1, t2)) lhss;
         val Ts = map fastype_of lhss;
         val tupleT = foldr1 HOLogic.mk_prodT Ts;
-        val aux_lhs = Free ("mutual_" ^ prefix, fastype_of arg --> tupleT) $ arg;
+        val aux_lhs = Free ("mutual_" ^ auxname, fastype_of arg --> tupleT) $ arg;
         val aux_eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
           (aux_lhs, foldr1 HOLogic.mk_prod rhss);
         fun mk_proj t [T] = [t]
@@ -223,7 +223,7 @@
         |-> (fn (aux_simp, proj_defs) => prove_eqs aux_simp proj_defs)
       end;
 
-fun random_aux_specification prefix eqs lthy =
+fun random_aux_specification prfx name eqs lthy =
   let
     val vs = fold Term.add_free_names ((snd o strip_comb o fst o HOLogic.dest_eq
       o HOLogic.dest_Trueprop o hd) eqs) [];
@@ -237,10 +237,10 @@
         val ext_simps = map (fn thm => fun_cong OF [fun_cong OF [thm]]) proto_simps;
         val tac = ALLGOALS (ProofContext.fact_tac ext_simps);
       in (map (fn prop => SkipProof.prove lthy vs [] prop (K tac)) eqs, lthy) end;
-    val b = Binding.qualify true prefix (Binding.name "simps");
+    val b = Binding.qualify true prfx (Binding.qualify true name (Binding.name "simps"));
   in
     lthy
-    |> random_aux_primrec_multi prefix proto_eqs
+    |> random_aux_primrec_multi (name ^ prfx) proto_eqs
     |-> (fn proto_simps => prove_simps proto_simps)
     |-> (fn simps => LocalTheory.note Thm.generatedK ((b,
            Code.add_default_eqn_attrib :: map (Attrib.internal o K)
@@ -252,6 +252,8 @@
 
 (* constructing random instances on datatypes *)
 
+val random_auxN = "random_aux";
+
 fun mk_random_aux_eqs thy descr vs tycos (names, auxnames) (Ts, Us) =
   let
     val mk_const = curry (Sign.mk_const thy);
@@ -259,7 +261,6 @@
     val i1 = @{term "(i\<Colon>code_numeral) - 1"};
     val j = @{term "j\<Colon>code_numeral"};
     val seed = @{term "s\<Colon>Random.seed"};
-    val random_auxN = "random_aux";
     val random_auxsN = map (prefix (random_auxN ^ "_")) (names @ auxnames);
     fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit \<Rightarrow> term"});
     val rTs = Ts @ Us;
@@ -316,10 +317,9 @@
           $ seed;
     val auxs_lhss = map (fn t => t $ i $ j $ seed) random_auxs;
     val auxs_rhss = map mk_select gen_exprss;
-    val prefix = space_implode "_" (random_auxN :: names);
-  in (prefix, (random_auxs, auxs_lhss ~~ auxs_rhss)) end;
+  in (random_auxs, auxs_lhss ~~ auxs_rhss) end;
 
-fun mk_random_datatype config descr vs tycos (names, auxnames) (Ts, Us) thy =
+fun mk_random_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
   let
     val _ = DatatypeAux.message config "Creating quickcheck generators ...";
     val i = @{term "i\<Colon>code_numeral"};
@@ -329,14 +329,14 @@
           else @{term "max :: code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"}
             $ HOLogic.mk_number @{typ code_numeral} l $ i
       | NONE => i;
-    val (prefix, (random_auxs, auxs_eqs)) = (apsnd o apsnd o map) mk_prop_eq
+    val (random_auxs, auxs_eqs) = (apsnd o map) mk_prop_eq
       (mk_random_aux_eqs thy descr vs tycos (names, auxnames) (Ts, Us));
     val random_defs = map_index (fn (k, T) => mk_prop_eq
       (HOLogic.mk_random T i, nth random_auxs k $ mk_size_arg k $ i)) Ts;
   in
     thy
     |> TheoryTarget.instantiation (tycos, vs, @{sort random})
-    |> random_aux_specification prefix auxs_eqs
+    |> random_aux_specification prfx random_auxN auxs_eqs
     |> `(fn lthy => map (Syntax.check_term lthy) random_defs)
     |-> (fn random_defs' => fold_map (fn random_def =>
           Specification.definition (NONE, (Attrib.empty_binding,
@@ -359,7 +359,7 @@
   let
     val pp = Syntax.pp_global thy;
     val algebra = Sign.classes_of thy;
-    val (descr, raw_vs, tycos, (names, auxnames), raw_TUs) =
+    val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) =
       Datatype.the_descr thy raw_tycos;
     val typrep_vs = (map o apsnd)
       (curry (Sorts.inter_sort algebra) @{sort typerep}) raw_vs;
@@ -374,7 +374,7 @@
   in if has_inst then thy
     else case perhaps_constrain thy (random_insts @ term_of_insts) typrep_vs
      of SOME constrain => mk_random_datatype config descr
-          (map constrain typrep_vs) tycos (names, auxnames)
+          (map constrain typrep_vs) tycos prfx (names, auxnames)
             ((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
       | NONE => thy
   end;
diff -r d262a0d46246 -r 3b08dcd74229 src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Tue Jun 30 11:21:02 2009 +0200
+++ b/src/Pure/Isar/class_target.ML	Tue Jun 30 14:54:32 2009 +0200
@@ -32,6 +32,7 @@
   (*instances*)
   val init_instantiation: string list * (string * sort) list * sort
     -> theory -> local_theory
+  val instance_arity_cmd: xstring list * xstring list * xstring -> theory -> Proof.state
   val instantiation_instance: (local_theory -> local_theory)
     -> local_theory -> Proof.state
   val prove_instantiation_instance: (Proof.context -> tactic)
@@ -44,7 +45,8 @@
   val instantiation_param: local_theory -> binding -> string option
   val confirm_declaration: binding -> local_theory -> local_theory
   val pretty_instantiation: local_theory -> Pretty.T
-  val instance_arity_cmd: xstring * xstring list * xstring -> theory -> Proof.state
+  val read_multi_arity: theory -> xstring list * xstring list * xstring
+    -> string list * (string * sort) list * sort
   val type_name: string -> string
 
   (*subclasses*)
@@ -419,6 +421,15 @@
   |> find_first (fn (_, (v, _)) => Binding.name_of b = v)
   |> Option.map (fst o fst);
 
+fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
+  let
+    val all_arities = map (fn raw_tyco => Sign.read_arity thy
+      (raw_tyco, raw_sorts, raw_sort)) raw_tycos;
+    val tycos = map #1 all_arities;
+    val (_, sorts, sort) = hd all_arities;
+    val vs = Name.names Name.context Name.aT sorts;
+  in (tycos, vs, sort) end;
+
 
 (* syntax *)
 
@@ -578,15 +589,17 @@
 
 (* simplified instantiation interface with no class parameter *)
 
-fun instance_arity_cmd arities thy =
+fun instance_arity_cmd raw_arities thy =
   let
+    val (tycos, vs, sort) = read_multi_arity thy raw_arities;
+    val sorts = map snd vs;
+    val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
     fun after_qed results = ProofContext.theory
       ((fold o fold) AxClass.add_arity results);
   in
     thy
     |> ProofContext.init
-    |> Proof.theorem_i NONE after_qed ((map (fn t => [(t, [])])
-        o Logic.mk_arities o Sign.read_arity thy) arities)
+    |> Proof.theorem_i NONE after_qed (map (fn t => [(t, [])]) arities)
   end;
 
 
diff -r d262a0d46246 -r 3b08dcd74229 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Jun 30 11:21:02 2009 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Jun 30 14:54:32 2009 +0200
@@ -465,7 +465,7 @@
 val _ =
   OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
   ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> Class.classrel_cmd ||
-    P.arity >> Class.instance_arity_cmd)
+    P.multi_arity >> Class.instance_arity_cmd)
     >> (Toplevel.print oo Toplevel.theory_to_proof)
   || Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
 
diff -r d262a0d46246 -r 3b08dcd74229 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Tue Jun 30 11:21:02 2009 +0200
+++ b/src/Pure/Isar/theory_target.ML	Tue Jun 30 14:54:32 2009 +0200
@@ -330,15 +330,6 @@
        else I)}
 and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta;
 
-fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
-  let
-    val all_arities = map (fn raw_tyco => Sign.read_arity thy
-      (raw_tyco, raw_sorts, raw_sort)) raw_tycos;
-    val tycos = map #1 all_arities;
-    val (_, sorts, sort) = hd all_arities;
-    val vs = Name.names Name.context Name.aT sorts;
-  in (tycos, vs, sort) end;
-
 fun gen_overloading prep_const raw_ops thy =
   let
     val ctxt = ProofContext.init thy;
@@ -356,7 +347,7 @@
 
 fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []);
 fun instantiation_cmd raw_arities thy =
-  instantiation (read_multi_arity thy raw_arities) thy;
+  instantiation (Class_Target.read_multi_arity thy raw_arities) thy;
 
 val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);
 val overloading_cmd = gen_overloading Syntax.read_term;
diff -r d262a0d46246 -r 3b08dcd74229 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Tue Jun 30 11:21:02 2009 +0200
+++ b/src/Tools/Code/code_haskell.ML	Tue Jun 30 14:54:32 2009 +0200
@@ -25,10 +25,8 @@
 
 fun pr_haskell_bind pr_term =
   let
-    fun pr_bind ((NONE, NONE), _) = str "_"
-      | pr_bind ((SOME v, NONE), _) = str v
-      | pr_bind ((NONE, SOME p), _) = p
-      | pr_bind ((SOME v, SOME p), _) = brackets [str v, str "@", p];
+    fun pr_bind (NONE, _) = str "_"
+      | pr_bind (SOME p, _) = p;
   in gen_pr_bind pr_bind pr_term end;
 
 fun pr_haskell_stmt labelled_name syntax_class syntax_tyco syntax_const
@@ -72,9 +70,8 @@
           (str o Code_Printer.lookup_var vars) v
       | pr_term tyvars thm vars fxy (t as _ `|=> _) =
           let
-            val (binds, t') = Code_Thingol.unfold_abs t;
-            fun pr ((v, pat), ty) = pr_bind tyvars thm BR ((SOME v, pat), ty);
-            val (ps, vars') = fold_map pr binds vars;
+            val (binds, t') = Code_Thingol.unfold_pat_abs t;
+            val (ps, vars') = fold_map (pr_bind tyvars thm BR) binds vars;
           in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars thm vars' NOBR t') end
       | pr_term tyvars thm vars fxy (ICase (cases as (_, t0))) =
           (case Code_Thingol.unfold_const_app t0
@@ -103,7 +100,7 @@
             val (binds, body) = Code_Thingol.unfold_let (ICase cases);
             fun pr ((pat, ty), t) vars =
               vars
-              |> pr_bind tyvars thm BR ((NONE, SOME pat), ty)
+              |> pr_bind tyvars thm BR (SOME pat, ty)
               |>> (fn p => semicolon [p, str "=", pr_term tyvars thm vars NOBR t])
             val (ps, vars') = fold_map pr binds vars;
           in brackify_block fxy (str "let {")
@@ -114,7 +111,7 @@
           let
             fun pr (pat, body) =
               let
-                val (p, vars') = pr_bind tyvars thm NOBR ((NONE, SOME pat), ty) vars;
+                val (p, vars') = pr_bind tyvars thm NOBR (SOME pat, ty) vars;
               in semicolon [p, str "->", pr_term tyvars thm vars' NOBR body] end;
           in brackify_block fxy
             (concat [str "case", pr_term tyvars thm vars NOBR t, str "of", str "{"])
@@ -240,8 +237,6 @@
           end
       | pr_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
           let
-            val split_abs_pure = (fn (v, _) `|=> t => SOME (v, t) | _ => NONE);
-            val unfold_abs_pure = Code_Thingol.unfoldr split_abs_pure;
             val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
             fun pr_instdef ((classparam, c_inst), (thm, _)) = case syntax_const classparam
              of NONE => semicolon [
@@ -255,7 +250,7 @@
                     val const = if (is_some o syntax_const) c_inst_name
                       then NONE else (SOME o Long_Name.base_name o deresolve) c_inst_name;
                     val proto_rhs = Code_Thingol.eta_expand k (c_inst, []);
-                    val (vs, rhs) = unfold_abs_pure proto_rhs;
+                    val (vs, rhs) = (apfst o map) fst (Code_Thingol.unfold_abs proto_rhs);
                     val vars = init_syms
                       |> Code_Printer.intro_vars (the_list const)
                       |> Code_Printer.intro_vars vs;
@@ -447,16 +442,16 @@
 
 fun pretty_haskell_monad c_bind =
   let
-    fun dest_bind t1 t2 = case Code_Thingol.split_abs t2
-     of SOME (((v, pat), ty), t') =>
-          SOME ((SOME (((SOME v, pat), ty), true), t1), t')
+    fun dest_bind t1 t2 = case Code_Thingol.split_pat_abs t2
+     of SOME ((some_pat, ty), t') =>
+          SOME ((SOME ((some_pat, ty), true), t1), t')
       | NONE => NONE;
     fun dest_monad c_bind_name (IConst (c, _) `$ t1 `$ t2) =
           if c = c_bind_name then dest_bind t1 t2
           else NONE
       | dest_monad _ t = case Code_Thingol.split_let t
          of SOME (((pat, ty), tbind), t') =>
-              SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t')
+              SOME ((SOME ((SOME pat, ty), false), tbind), t')
           | NONE => NONE;
     fun implode_monad c_bind_name = Code_Thingol.unfoldr (dest_monad c_bind_name);
     fun pr_monad pr_bind pr (NONE, t) vars =
diff -r d262a0d46246 -r 3b08dcd74229 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Tue Jun 30 11:21:02 2009 +0200
+++ b/src/Tools/Code/code_ml.ML	Tue Jun 30 14:54:32 2009 +0200
@@ -94,9 +94,9 @@
                [pr_term is_closure thm vars NOBR t1, pr_term is_closure thm vars BR t2])
       | pr_term is_closure thm vars fxy (t as _ `|=> _) =
           let
-            val (binds, t') = Code_Thingol.unfold_abs t;
-            fun pr ((v, pat), ty) =
-              pr_bind is_closure thm NOBR ((SOME v, pat), ty)
+            val (binds, t') = Code_Thingol.unfold_pat_abs t;
+            fun pr (some_pat, ty) =
+              pr_bind is_closure thm NOBR (some_pat, ty)
               #>> (fn p => concat [str "fn", p, str "=>"]);
             val (ps, vars') = fold_map pr binds vars;
           in brackets (ps @ [pr_term is_closure thm vars' NOBR t']) end
@@ -122,17 +122,15 @@
           :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term is_closure thm vars BR) ts
     and pr_app is_closure thm vars = gen_pr_app (pr_app' is_closure) (pr_term is_closure)
       syntax_const thm vars
-    and pr_bind' ((NONE, NONE), _) = str "_"
-      | pr_bind' ((SOME v, NONE), _) = str v
-      | pr_bind' ((NONE, SOME p), _) = p
-      | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p]
+    and pr_bind' (NONE, _) = str "_"
+      | pr_bind' (SOME p, _) = p
     and pr_bind is_closure = gen_pr_bind pr_bind' (pr_term is_closure)
     and pr_case is_closure thm vars fxy (cases as ((_, [_]), _)) =
           let
             val (binds, body) = Code_Thingol.unfold_let (ICase cases);
             fun pr ((pat, ty), t) vars =
               vars
-              |> pr_bind is_closure thm NOBR ((NONE, SOME pat), ty)
+              |> pr_bind is_closure thm NOBR (SOME pat, ty)
               |>> (fn p => semicolon [str "val", p, str "=", pr_term is_closure thm vars NOBR t])
             val (ps, vars') = fold_map pr binds vars;
           in
@@ -146,7 +144,7 @@
           let
             fun pr delim (pat, body) =
               let
-                val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars;
+                val (p, vars') = pr_bind is_closure thm NOBR (SOME pat, ty) vars;
               in
                 concat [str delim, p, str "=>", pr_term is_closure thm vars' NOBR body]
               end;
@@ -403,9 +401,8 @@
                 brackify fxy [pr_term is_closure thm vars NOBR t1, pr_term is_closure thm vars BR t2])
       | pr_term is_closure thm vars fxy (t as _ `|=> _) =
           let
-            val (binds, t') = Code_Thingol.unfold_abs t;
-            fun pr ((v, pat), ty) = pr_bind is_closure thm BR ((SOME v, pat), ty);
-            val (ps, vars') = fold_map pr binds vars;
+            val (binds, t') = Code_Thingol.unfold_pat_abs t;
+            val (ps, vars') = fold_map (pr_bind is_closure thm BR) binds vars;
           in brackets (str "fun" :: ps @ str "->" @@ pr_term is_closure thm vars' NOBR t') end
       | pr_term is_closure thm vars fxy (ICase (cases as (_, t0))) = (case Code_Thingol.unfold_const_app t0
            of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
@@ -427,17 +424,15 @@
         :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term is_closure thm vars BR) ts)
     and pr_app is_closure = gen_pr_app (pr_app' is_closure) (pr_term is_closure)
       syntax_const
-    and pr_bind' ((NONE, NONE), _) = str "_"
-      | pr_bind' ((SOME v, NONE), _) = str v
-      | pr_bind' ((NONE, SOME p), _) = p
-      | pr_bind' ((SOME v, SOME p), _) = brackets [p, str "as", str v]
+    and pr_bind' (NONE, _) = str "_"
+      | pr_bind' (SOME p, _) = p
     and pr_bind is_closure = gen_pr_bind pr_bind' (pr_term is_closure)
     and pr_case is_closure thm vars fxy (cases as ((_, [_]), _)) =
           let
             val (binds, body) = Code_Thingol.unfold_let (ICase cases);
             fun pr ((pat, ty), t) vars =
               vars
-              |> pr_bind is_closure thm NOBR ((NONE, SOME pat), ty)
+              |> pr_bind is_closure thm NOBR (SOME pat, ty)
               |>> (fn p => concat
                   [str "let", p, str "=", pr_term is_closure thm vars NOBR t, str "in"])
             val (ps, vars') = fold_map pr binds vars;
@@ -449,7 +444,7 @@
           let
             fun pr delim (pat, body) =
               let
-                val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars;
+                val (p, vars') = pr_bind is_closure thm NOBR (SOME pat, ty) vars;
               in concat [str delim, p, str "->", pr_term is_closure thm vars' NOBR body] end;
           in
             brackets (
diff -r d262a0d46246 -r 3b08dcd74229 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Tue Jun 30 11:21:02 2009 +0200
+++ b/src/Tools/Code/code_printer.ML	Tue Jun 30 14:54:32 2009 +0200
@@ -68,10 +68,10 @@
     -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
     -> (string -> const_syntax option)
     -> thm -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
-  val gen_pr_bind: ((string option * Pretty.T option) * itype -> Pretty.T)
+  val gen_pr_bind: (Pretty.T option * itype -> Pretty.T)
     -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
     -> thm -> fixity
-    -> (string option * iterm option) * itype -> var_ctxt -> Pretty.T * var_ctxt
+    -> iterm option * itype -> var_ctxt -> Pretty.T * var_ctxt
 
   val mk_name_module: Name.context -> string option -> (string -> string option)
     -> 'a Graph.T -> string -> string
@@ -216,16 +216,14 @@
           else pr_term thm vars fxy (Code_Thingol.eta_expand k app)
         end;
 
-fun gen_pr_bind pr_bind pr_term thm (fxy : fixity) ((v, pat), ty : itype) vars =
+fun gen_pr_bind pr_bind pr_term thm (fxy : fixity) (some_pat, ty : itype) vars =
   let
-    val vs = case pat
+    val vs = case some_pat
      of SOME pat => Code_Thingol.fold_varnames (insert (op =)) pat []
       | NONE => [];
-    val vars' = intro_vars (the_list v) vars;
-    val vars'' = intro_vars vs vars';
-    val v' = Option.map (lookup_var vars') v;
-    val pat' = Option.map (pr_term thm vars'' fxy) pat;
-  in (pr_bind ((v', pat'), ty), vars'') end;
+    val vars' = intro_vars vs vars;
+    val some_pat' = Option.map (pr_term thm vars' fxy) some_pat;
+  in (pr_bind (some_pat', ty), vars') end;
 
 
 (* mixfix syntax *)
diff -r d262a0d46246 -r 3b08dcd74229 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Tue Jun 30 11:21:02 2009 +0200
+++ b/src/Tools/Code/code_thingol.ML	Tue Jun 30 14:54:32 2009 +0200
@@ -40,13 +40,12 @@
   val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a
   val unfold_fun: itype -> itype list * itype
   val unfold_app: iterm -> iterm * iterm list
-  val split_abs: iterm -> (((vname * iterm option) * itype) * iterm) option
-  val unfold_abs: iterm -> ((vname * iterm option) * itype) list * iterm
+  val unfold_abs: iterm -> (vname * itype) list * iterm
   val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option
   val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm
+  val split_pat_abs: iterm -> ((iterm option * itype) * iterm) option
+  val unfold_pat_abs: iterm -> (iterm option * itype) list * iterm
   val unfold_const_app: iterm -> (const * iterm list) option
-  val collapse_let: ((vname * itype) * iterm) * iterm
-    -> (iterm * itype) * (iterm * iterm) list
   val eta_expand: int -> const * iterm list -> iterm
   val contains_dictvar: iterm -> bool
   val locally_monomorphic: iterm -> bool
@@ -139,14 +138,10 @@
   (fn op `$ t => SOME t
     | _ => NONE);
 
-val split_abs =
-  (fn (v, ty) `|=> (t as ICase (((IVar w, _), [(p, t')]), _)) =>
-        if v = w then SOME (((v, SOME p), ty), t') else SOME (((v, NONE), ty), t)
-    | (v, ty) `|=> t => SOME (((v, NONE), ty), t)
+val unfold_abs = unfoldr
+  (fn op `|=> t => SOME t
     | _ => NONE);
 
-val unfold_abs = unfoldr split_abs;
-
 val split_let = 
   (fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t)
     | _ => NONE);
@@ -186,17 +181,17 @@
       | add vs (ICase (_, t)) = add vs t;
   in add [] end;
 
-fun collapse_let (((v, ty), se), be as ICase (((IVar w, _), ds), _)) =
-      let
-        fun exists_v t = fold_unbound_varnames (fn w => fn b =>
-          b orelse v = w) t false;
-      in if v = w andalso forall (fn (t1, t2) =>
-        exists_v t1 orelse not (exists_v t2)) ds
-        then ((se, ty), ds)
-        else ((se, ty), [(IVar v, be)])
-      end
-  | collapse_let (((v, ty), se), be) =
-      ((se, ty), [(IVar v, be)])
+fun exists_var t v = fold_unbound_varnames (fn w => fn b => v = w orelse b) t false;
+
+val split_pat_abs = (fn (v, ty) `|=> t => (case t
+   of ICase (((IVar w, _), [(p, t')]), _) =>
+        if v = w andalso (exists_var p v orelse not (exists_var t' v))
+        then SOME ((SOME p, ty), t')
+        else SOME ((SOME (IVar v), ty), t)
+    | _ => SOME ((if exists_var t v then SOME (IVar v) else NONE, ty), t))
+  | _ => NONE);
+
+val unfold_pat_abs = unfoldr split_pat_abs;
 
 fun eta_expand k (c as (_, (_, tys)), ts) =
   let