merged
authorblanchet
Wed, 30 Jun 2010 18:19:53 +0200
changeset 37644 48bdc2a43b46
parent 37641 39bd6f7c25c2 (diff)
parent 37643 f576af716aa6 (current diff)
child 37645 5cbd5d5959f2
merged
--- a/src/HOL/Quotient_Examples/FSet.thy	Wed Jun 30 18:03:34 2010 +0200
+++ b/src/HOL/Quotient_Examples/FSet.thy	Wed Jun 30 18:19:53 2010 +0200
@@ -379,50 +379,6 @@
 
 text {* Distributive lattice with bot *}
 
-lemma sub_list_not_eq:
-  "(sub_list x y \<and> \<not> list_eq x y) = (sub_list x y \<and> \<not> sub_list y x)"
-  by (auto simp add: sub_list_def)
-
-lemma sub_list_refl:
-  "sub_list x x"
-  by (simp add: sub_list_def)
-
-lemma sub_list_trans:
-  "sub_list x y \<Longrightarrow> sub_list y z \<Longrightarrow> sub_list x z"
-  by (simp add: sub_list_def)
-
-lemma sub_list_empty:
-  "sub_list [] x"
-  by (simp add: sub_list_def)
-
-lemma sub_list_append_left:
-  "sub_list x (x @ y)"
-  by (simp add: sub_list_def)
-
-lemma sub_list_append_right:
-  "sub_list y (x @ y)"
-  by (simp add: sub_list_def)
-
-lemma sub_list_inter_left:
-  shows "sub_list (finter_raw x y) x"
-  by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
-
-lemma sub_list_inter_right:
-  shows "sub_list (finter_raw x y) y"
-  by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
-
-lemma sub_list_list_eq:
-  "sub_list x y \<Longrightarrow> sub_list y x \<Longrightarrow> list_eq x y"
-  unfolding sub_list_def list_eq.simps by blast
-
-lemma sub_list_append:
-  "sub_list y x \<Longrightarrow> sub_list z x \<Longrightarrow> sub_list (y @ z) x"
-  unfolding sub_list_def by auto
-
-lemma sub_list_inter:
-  "sub_list x y \<Longrightarrow> sub_list x z \<Longrightarrow> sub_list x (finter_raw y z)"
-  by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
-
 lemma append_inter_distrib:
   "x @ (finter_raw y z) \<approx> finter_raw (x @ y) (x @ z)"
   apply (induct x)
@@ -431,7 +387,7 @@
   apply (auto simp add: memb_def)
   done
 
-instantiation fset :: (type) "{bounded_lattice_bot,distrib_lattice,minus}"
+instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}"
 begin
 
 quotient_definition
@@ -482,42 +438,50 @@
   "xs |\<inter>| ys \<equiv> inf (xs :: 'a fset) ys"
 
 quotient_definition
-  "minus \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)"
+  "minus :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 is
-  "fminus_raw \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> 'a list)"
+  "fminus_raw :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 
 instance
 proof
   fix x y z :: "'a fset"
-  show "(x |\<subset>| y) = (x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x)"
-    unfolding less_fset by (lifting sub_list_not_eq)
-  show "x |\<subseteq>| x" by (lifting sub_list_refl)
-  show "{||} |\<subseteq>| x" by (lifting sub_list_empty)
-  show "x |\<subseteq>| x |\<union>| y" by (lifting sub_list_append_left)
-  show "y |\<subseteq>| x |\<union>| y" by (lifting sub_list_append_right)
-  show "x |\<inter>| y |\<subseteq>| x" by (lifting sub_list_inter_left)
-  show "x |\<inter>| y |\<subseteq>| y" by (lifting sub_list_inter_right)
-  show "x |\<union>| (y |\<inter>| z) = x |\<union>| y |\<inter>| (x |\<union>| z)" by (lifting append_inter_distrib)
+  show "x |\<subset>| y \<longleftrightarrow> x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x"
+    unfolding less_fset 
+    by (descending) (auto simp add: sub_list_def)
+  show "x |\<subseteq>| x"  by (descending) (simp add: sub_list_def)
+  show "{||} |\<subseteq>| x" by (descending) (simp add: sub_list_def)
+  show "x |\<subseteq>| x |\<union>| y" by (descending) (simp add: sub_list_def)
+  show "y |\<subseteq>| x |\<union>| y" by (descending) (simp add: sub_list_def)
+  show "x |\<inter>| y |\<subseteq>| x" 
+    by (descending) (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
+  show "x |\<inter>| y |\<subseteq>| y" 
+    by (descending) (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
+  show "x |\<union>| (y |\<inter>| z) = x |\<union>| y |\<inter>| (x |\<union>| z)" 
+    by (descending) (rule append_inter_distrib)
 next
   fix x y z :: "'a fset"
   assume a: "x |\<subseteq>| y"
   assume b: "y |\<subseteq>| z"
-  show "x |\<subseteq>| z" using a b by (lifting sub_list_trans)
+  show "x |\<subseteq>| z" using a b 
+    by (descending) (simp add: sub_list_def)
 next
   fix x y :: "'a fset"
   assume a: "x |\<subseteq>| y"
   assume b: "y |\<subseteq>| x"
-  show "x = y" using a b by (lifting sub_list_list_eq)
+  show "x = y" using a b 
+    by (descending) (unfold sub_list_def list_eq.simps, blast)
 next
   fix x y z :: "'a fset"
   assume a: "y |\<subseteq>| x"
   assume b: "z |\<subseteq>| x"
-  show "y |\<union>| z |\<subseteq>| x" using a b by (lifting sub_list_append)
+  show "y |\<union>| z |\<subseteq>| x" using a b 
+    by (descending) (simp add: sub_list_def)
 next
   fix x y z :: "'a fset"
   assume a: "x |\<subseteq>| y"
   assume b: "x |\<subseteq>| z"
-  show "x |\<subseteq>| y |\<inter>| z" using a b by (lifting sub_list_inter)
+  show "x |\<subseteq>| y |\<inter>| z" using a b 
+    by (descending) (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
 qed
 
 end
@@ -750,14 +714,6 @@
   "memb x (xs @ ys) \<longleftrightarrow> memb x xs \<or> memb x ys"
   by (induct xs) (simp_all add: not_memb_nil memb_cons_iff)
 
-lemma cons_left_comm:
-  "x # y # xs \<approx> y # x # xs"
-  by auto
-
-lemma cons_left_idem:
-  "x # x # xs \<approx> x # xs"
-  by auto
-
 lemma fset_raw_strong_cases:
   obtains "xs = []"
     | x ys where "\<not> memb x ys" and "xs \<approx> x # ys"
@@ -809,10 +765,6 @@
   "fcard_raw (delete_raw xs y) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
   by (simp add: fdelete_raw_filter fcard_raw_delete_one)
 
-lemma finter_raw_empty:
-  "finter_raw l [] = []"
-  by (induct l) (simp_all add: not_memb_nil)
-
 lemma set_cong:
   shows "(x \<approx> y) = (set x = set y)"
   by auto
@@ -903,7 +855,7 @@
 text {* Set *}
 
 lemma sub_list_set: "sub_list xs ys = (set xs \<subseteq> set ys)"
-  by (metis rev_append set_append set_cong set_rev sub_list_append sub_list_append_left sub_list_def sub_list_not_eq subset_Un_eq)
+  unfolding sub_list_def by auto
 
 lemma sub_list_neq_set: "(sub_list xs ys \<and> \<not> list_eq xs ys) = (set xs \<subset> set ys)"
   by (auto simp add: sub_list_set)
@@ -939,20 +891,20 @@
 text {* Lifted theorems *}
 
 lemma not_fin_fnil: "x |\<notin>| {||}"
-  by (lifting not_memb_nil)
+  by (descending) (simp add: memb_def)
 
 lemma fin_finsert_iff[simp]:
-  "x |\<in>| finsert y S = (x = y \<or> x |\<in>| S)"
-  by (lifting memb_cons_iff)
+  "x |\<in>| finsert y S \<longleftrightarrow> x = y \<or> x |\<in>| S"
+  by (descending) (simp add: memb_def)
 
 lemma
   shows finsertI1: "x |\<in>| finsert x S"
   and   finsertI2: "x |\<in>| S \<Longrightarrow> x |\<in>| finsert y S"
-  by (lifting memb_consI1, lifting memb_consI2)
+  by (lifting memb_consI1 memb_consI2)
 
 lemma finsert_absorb[simp]:
   shows "x |\<in>| S \<Longrightarrow> finsert x S = S"
-  by (lifting memb_absorb)
+  by (descending) (auto simp add: memb_def)
 
 lemma fempty_not_finsert[simp]:
   "{||} \<noteq> finsert x S"
@@ -961,21 +913,23 @@
 
 lemma finsert_left_comm:
   "finsert x (finsert y S) = finsert y (finsert x S)"
-  by (lifting cons_left_comm)
+  by (descending) (auto)
 
 lemma finsert_left_idem:
   "finsert x (finsert x S) = finsert x S"
-  by (lifting cons_left_idem)
+  by (descending) (auto)
 
 lemma fsingleton_eq[simp]:
   shows "{|x|} = {|y|} \<longleftrightarrow> x = y"
-  by (lifting singleton_list_eq)
+  by (descending) (auto)
+
 
 text {* fset_to_set *}
 
-lemma fset_to_set_simps[simp]:
-  "fset_to_set {||} = ({} :: 'a set)"
-  "fset_to_set (finsert (h :: 'a) t) = insert h (fset_to_set t)"
+lemma fset_to_set_simps [simp]:
+  fixes h::"'a"
+  shows "fset_to_set {||} = ({} :: 'a set)"
+  and "fset_to_set (finsert h t) = insert h (fset_to_set t)"
   by (lifting set.simps)
 
 lemma in_fset_to_set:
@@ -983,28 +937,29 @@
   by (lifting memb_def[symmetric])
 
 lemma none_fin_fempty:
-  "(\<forall>x. x |\<notin>| S) = (S = {||})"
+  "(\<forall>x. x |\<notin>| S) \<longleftrightarrow> S = {||}"
   by (lifting none_memb_nil)
 
 lemma fset_cong:
-  "(S = T) = (fset_to_set S = fset_to_set T)"
+  "S = T \<longleftrightarrow> fset_to_set S = fset_to_set T"
   by (lifting set_cong)
 
 text {* fcard *}
 
 lemma fcard_fempty [simp]:
   shows "fcard {||} = 0"
-  by (lifting fcard_raw_nil)
+  by (descending) (simp)
 
 lemma fcard_finsert_if [simp]:
   shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))"
-  by (lifting fcard_raw_cons)
+  by (descending) (simp)
 
-lemma fcard_0: "(fcard S = 0) = (S = {||})"
+lemma fcard_0: 
+  "fcard S = 0 \<longleftrightarrow> S = {||}"
   by (lifting fcard_raw_0)
 
 lemma fcard_1:
-  shows "(fcard S = 1) = (\<exists>x. S = {|x|})"
+  shows "fcard S = 1 \<longleftrightarrow> (\<exists>x. S = {|x|})"
   by (lifting fcard_raw_1)
 
 lemma fcard_gt_0:
@@ -1039,11 +994,11 @@
   by (lifting append.simps(2))
 
 lemma singleton_union_left:
-  "{|a|} |\<union>| S = finsert a S"
+  shows "{|a|} |\<union>| S = finsert a S"
   by simp
 
 lemma singleton_union_right:
-  "S |\<union>| {|a|} = finsert a S"
+  shows "S |\<union>| {|a|} = finsert a S"
   by (subst sup.commute) simp
 
 section {* Induction and Cases rules for finite sets *}
@@ -1105,8 +1060,9 @@
 text {* fmap *}
 
 lemma fmap_simps[simp]:
-  "fmap (f :: 'a \<Rightarrow> 'b) {||} = {||}"
-  "fmap f (finsert x S) = finsert (f x) (fmap f S)"
+  fixes f::"'a \<Rightarrow> 'b"
+  shows "fmap f {||} = {||}"
+  and   "fmap f (finsert x S) = finsert (f x) (fmap f S)"
   by (lifting map.simps)
 
 lemma fmap_set_image:
@@ -1114,51 +1070,62 @@
   by (induct S) simp_all
 
 lemma inj_fmap_eq_iff:
-  "inj f \<Longrightarrow> (fmap f S = fmap f T) = (S = T)"
+  "inj f \<Longrightarrow> fmap f S = fmap f T \<longleftrightarrow> S = T"
   by (lifting inj_map_eq_iff)
 
-lemma fmap_funion: "fmap f (S |\<union>| T) = fmap f S |\<union>| fmap f T"
+lemma fmap_funion: 
+  shows "fmap f (S |\<union>| T) = fmap f S |\<union>| fmap f T"
   by (lifting map_append)
 
 lemma fin_funion:
-  "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
+  shows "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
   by (lifting memb_append)
 
 text {* to_set *}
 
-lemma fin_set: "(x |\<in>| xs) = (x \<in> fset_to_set xs)"
+lemma fin_set: 
+  shows "x |\<in>| xs \<longleftrightarrow> x \<in> fset_to_set xs"
   by (lifting memb_set)
 
-lemma fnotin_set: "(x |\<notin>| xs) = (x \<notin> fset_to_set xs)"
+lemma fnotin_set: 
+  shows "x |\<notin>| xs \<longleftrightarrow> x \<notin> fset_to_set xs"
   by (simp add: fin_set)
 
-lemma fcard_set: "fcard xs = card (fset_to_set xs)"
+lemma fcard_set: 
+  shows "fcard xs = card (fset_to_set xs)"
   by (lifting fcard_raw_set)
 
-lemma fsubseteq_set: "(xs |\<subseteq>| ys) = (fset_to_set xs \<subseteq> fset_to_set ys)"
+lemma fsubseteq_set: 
+  shows "xs |\<subseteq>| ys \<longleftrightarrow> fset_to_set xs \<subseteq> fset_to_set ys"
   by (lifting sub_list_set)
 
-lemma fsubset_set: "(xs |\<subset>| ys) = (fset_to_set xs \<subset> fset_to_set ys)"
+lemma fsubset_set: 
+  shows "xs |\<subset>| ys \<longleftrightarrow> fset_to_set xs \<subset> fset_to_set ys"
   unfolding less_fset by (lifting sub_list_neq_set)
 
-lemma ffilter_set: "fset_to_set (ffilter P xs) = P \<inter> fset_to_set xs"
+lemma ffilter_set: 
+  shows "fset_to_set (ffilter P xs) = P \<inter> fset_to_set xs"
   by (lifting filter_set)
 
-lemma fdelete_set: "fset_to_set (fdelete xs x) = fset_to_set xs - {x}"
+lemma fdelete_set: 
+  shows "fset_to_set (fdelete xs x) = fset_to_set xs - {x}"
   by (lifting delete_raw_set)
 
-lemma inter_set: "fset_to_set (xs |\<inter>| ys) = fset_to_set xs \<inter> fset_to_set ys"
+lemma finter_set: 
+  shows "fset_to_set (xs |\<inter>| ys) = fset_to_set xs \<inter> fset_to_set ys"
   by (lifting inter_raw_set)
 
-lemma union_set: "fset_to_set (xs |\<union>| ys) = fset_to_set xs \<union> fset_to_set ys"
+lemma funion_set: 
+  shows "fset_to_set (xs |\<union>| ys) = fset_to_set xs \<union> fset_to_set ys"
   by (lifting set_append)
 
-lemma fminus_set: "fset_to_set (xs - ys) = fset_to_set xs - fset_to_set ys"
+lemma fminus_set: 
+  shows "fset_to_set (xs - ys) = fset_to_set xs - fset_to_set ys"
   by (lifting fminus_raw_set)
 
 lemmas fset_to_set_trans =
   fin_set fnotin_set fcard_set fsubseteq_set fsubset_set
-  inter_set union_set ffilter_set fset_to_set_simps
+  finter_set funion_set ffilter_set fset_to_set_simps
   fset_cong fdelete_set fmap_set_image fminus_set
 
 
@@ -1193,13 +1160,16 @@
   shows "S = {||} \<or> (\<exists>x. x |\<in>| S \<and> S = finsert x (fdelete S x))"
   by (lifting fset_raw_delete_raw_cases)
 
-text {* inter *}
+text {* finite intersection *}
 
-lemma finter_empty_l: "({||} |\<inter>| S) = {||}"
-  by (lifting finter_raw.simps(1))
+lemma finter_empty_l: 
+  shows "{||} |\<inter>| S = {||}"
+  by simp
 
-lemma finter_empty_r: "(S |\<inter>| {||}) = {||}"
-  by (lifting finter_raw_empty)
+
+lemma finter_empty_r: 
+  shows "S |\<inter>| {||} = {||}"
+  by simp
 
 lemma finter_finsert:
   "finsert x S |\<inter>| T = (if x |\<in>| T then finsert x (S |\<inter>| T) else S |\<inter>| T)"
@@ -1210,30 +1180,36 @@
   by (lifting memb_finter_raw)
 
 lemma fsubset_finsert:
-  "(finsert x xs |\<subseteq>| ys) = (x |\<in>| ys \<and> xs |\<subseteq>| ys)"
+  shows "finsert x xs |\<subseteq>| ys \<longleftrightarrow> x |\<in>| ys \<and> xs |\<subseteq>| ys"
   by (lifting sub_list_cons)
 
-lemma "xs |\<subseteq>| ys \<equiv> \<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys"
+lemma 
+  shows "xs |\<subseteq>| ys \<equiv> \<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys"
   by (lifting sub_list_def[simplified memb_def[symmetric]])
 
-lemma fsubset_fin: "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)"
+lemma fsubset_fin: 
+  shows "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)"
 by (rule meta_eq_to_obj_eq)
    (lifting sub_list_def[simplified memb_def[symmetric]])
 
-lemma fminus_fin: "(x |\<in>| xs - ys) = (x |\<in>| xs \<and> x |\<notin>| ys)"
+lemma fminus_fin: 
+  shows "x |\<in>| xs - ys \<longleftrightarrow> x |\<in>| xs \<and> x |\<notin>| ys"
   by (lifting fminus_raw_memb)
 
-lemma fminus_red: "finsert x xs - ys = (if x |\<in>| ys then xs - ys else finsert x (xs - ys))"
+lemma fminus_red: 
+  shows "finsert x xs - ys = (if x |\<in>| ys then xs - ys else finsert x (xs - ys))"
   by (lifting fminus_raw_red)
 
-lemma fminus_red_fin[simp]: "x |\<in>| ys \<Longrightarrow> finsert x xs - ys = xs - ys"
+lemma fminus_red_fin [simp]: 
+  shows "x |\<in>| ys \<Longrightarrow> finsert x xs - ys = xs - ys"
   by (simp add: fminus_red)
 
-lemma fminus_red_fnotin[simp]: "x |\<notin>| ys \<Longrightarrow> finsert x xs - ys = finsert x (xs - ys)"
+lemma fminus_red_fnotin[simp]: 
+  shows "x |\<notin>| ys \<Longrightarrow> finsert x xs - ys = finsert x (xs - ys)"
   by (simp add: fminus_red)
 
 lemma expand_fset_eq:
-  "(S = T) = (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
+  shows "S = T \<longleftrightarrow> (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
   by (lifting list_eq.simps[simplified memb_def[symmetric]])
 
 (* We cannot write it as "assumes .. shows" since Isabelle changes
@@ -1261,7 +1237,7 @@
   using assms
   by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]])
 
-text {* concat *}
+section {* fconcat *}
 
 lemma fconcat_empty:
   shows "fconcat {||} = {||}"
@@ -1271,19 +1247,24 @@
   shows "fconcat (finsert x S) = x |\<union>| fconcat S"
   by (lifting concat.simps(2))
 
-lemma "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys"
+lemma 
+  shows "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys"
   by (lifting concat_append)
 
-text {* ffilter *}
+
+section {* ffilter *}
 
-lemma subseteq_filter: "ffilter P xs <= ffilter Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
-by (lifting sub_list_filter)
+lemma subseteq_filter: 
+  shows "ffilter P xs <= ffilter Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
+  by (lifting sub_list_filter)
 
-lemma eq_ffilter: "(ffilter P xs = ffilter Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"
-by (lifting list_eq_filter)
+lemma eq_ffilter: 
+  shows "(ffilter P xs = ffilter Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"
+  by (lifting list_eq_filter)
 
-lemma subset_ffilter: "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> ffilter P xs < ffilter Q xs"
-unfolding less_fset by (auto simp add: subseteq_filter eq_ffilter)
+lemma subset_ffilter: 
+  shows "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> ffilter P xs < ffilter Q xs"
+  unfolding less_fset by (auto simp add: subseteq_filter eq_ffilter)
 
 section {* lemmas transferred from Finite_Set theory *}
 
@@ -1291,67 +1272,82 @@
 lemma finite_fset: "finite (fset_to_set S)"
   by (induct S) auto
 
-lemma fset_choice: "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)"
+lemma fset_choice: 
+  shows "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)"
   unfolding fset_to_set_trans
   by (rule finite_set_choice[simplified Ball_def, OF finite_fset])
 
-lemma fsubseteq_fnil: "xs |\<subseteq>| {||} = (xs = {||})"
+lemma fsubseteq_fnil: 
+  shows "xs |\<subseteq>| {||} \<longleftrightarrow> xs = {||}"
   unfolding fset_to_set_trans
   by (rule subset_empty)
 
-lemma not_fsubset_fnil: "\<not> xs |\<subset>| {||}"
+lemma not_fsubset_fnil: 
+  shows "\<not> xs |\<subset>| {||}"
   unfolding fset_to_set_trans
   by (rule not_psubset_empty)
 
-lemma fcard_mono: "xs |\<subseteq>| ys \<Longrightarrow> fcard xs \<le> fcard ys"
+lemma fcard_mono: 
+  shows "xs |\<subseteq>| ys \<Longrightarrow> fcard xs \<le> fcard ys"
   unfolding fset_to_set_trans
   by (rule card_mono[OF finite_fset])
 
-lemma fcard_fseteq: "xs |\<subseteq>| ys \<Longrightarrow> fcard ys \<le> fcard xs \<Longrightarrow> xs = ys"
+lemma fcard_fseteq: 
+  shows "xs |\<subseteq>| ys \<Longrightarrow> fcard ys \<le> fcard xs \<Longrightarrow> xs = ys"
   unfolding fset_to_set_trans
   by (rule card_seteq[OF finite_fset])
 
-lemma psubset_fcard_mono: "xs |\<subset>| ys \<Longrightarrow> fcard xs < fcard ys"
+lemma psubset_fcard_mono: 
+  shows "xs |\<subset>| ys \<Longrightarrow> fcard xs < fcard ys"
   unfolding fset_to_set_trans
   by (rule psubset_card_mono[OF finite_fset])
 
-lemma fcard_funion_finter: "fcard xs + fcard ys = fcard (xs |\<union>| ys) + fcard (xs |\<inter>| ys)"
+lemma fcard_funion_finter: 
+  shows "fcard xs + fcard ys = fcard (xs |\<union>| ys) + fcard (xs |\<inter>| ys)"
   unfolding fset_to_set_trans
   by (rule card_Un_Int[OF finite_fset finite_fset])
 
-lemma fcard_funion_disjoint: "xs |\<inter>| ys = {||} \<Longrightarrow> fcard (xs |\<union>| ys) = fcard xs + fcard ys"
+lemma fcard_funion_disjoint: 
+  shows "xs |\<inter>| ys = {||} \<Longrightarrow> fcard (xs |\<union>| ys) = fcard xs + fcard ys"
   unfolding fset_to_set_trans
   by (rule card_Un_disjoint[OF finite_fset finite_fset])
 
-lemma fcard_delete1_less: "x |\<in>| xs \<Longrightarrow> fcard (fdelete xs x) < fcard xs"
+lemma fcard_delete1_less: 
+  shows "x |\<in>| xs \<Longrightarrow> fcard (fdelete xs x) < fcard xs"
   unfolding fset_to_set_trans
   by (rule card_Diff1_less[OF finite_fset])
 
-lemma fcard_delete2_less: "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> fcard (fdelete (fdelete xs x) y) < fcard xs"
+lemma fcard_delete2_less: 
+  shows "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> fcard (fdelete (fdelete xs x) y) < fcard xs"
   unfolding fset_to_set_trans
   by (rule card_Diff2_less[OF finite_fset])
 
-lemma fcard_delete1_le: "fcard (fdelete xs x) <= fcard xs"
+lemma fcard_delete1_le: 
+  shows "fcard (fdelete xs x) \<le> fcard xs"
   unfolding fset_to_set_trans
   by (rule card_Diff1_le[OF finite_fset])
 
-lemma fcard_psubset: "ys |\<subseteq>| xs \<Longrightarrow> fcard ys < fcard xs \<Longrightarrow> ys |\<subset>| xs"
+lemma fcard_psubset: 
+  shows "ys |\<subseteq>| xs \<Longrightarrow> fcard ys < fcard xs \<Longrightarrow> ys |\<subset>| xs"
   unfolding fset_to_set_trans
   by (rule card_psubset[OF finite_fset])
 
-lemma fcard_fmap_le: "fcard (fmap f xs) \<le> fcard xs"
+lemma fcard_fmap_le: 
+  shows "fcard (fmap f xs) \<le> fcard xs"
   unfolding fset_to_set_trans
   by (rule card_image_le[OF finite_fset])
 
-lemma fin_fminus_fnotin: "x |\<in>| F - S \<Longrightarrow> x |\<notin>| S"
+lemma fin_fminus_fnotin: 
+  shows "x |\<in>| F - S \<Longrightarrow> x |\<notin>| S"
   unfolding fset_to_set_trans
   by blast
 
-lemma fin_fnotin_fminus: "x |\<in>| S \<Longrightarrow> x |\<notin>| F - S"
+lemma fin_fnotin_fminus: 
+  shows "x |\<in>| S \<Longrightarrow> x |\<notin>| F - S"
   unfolding fset_to_set_trans
   by blast
 
-lemma fin_mdef: "x |\<in>| F = ((x |\<notin>| (F - {|x|})) & (F = finsert x (F - {|x|})))"
+lemma fin_mdef: "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = finsert x (F - {|x|})"
   unfolding fset_to_set_trans
   by blast
 
@@ -1370,7 +1366,7 @@
 lemma fcard_fminus_subset_finter:
   "fcard (A - B) = fcard A - fcard (A |\<inter>| B)"
   unfolding fset_to_set_trans
-  by (rule card_Diff_subset_Int) (fold inter_set, rule finite_fset)
+  by (rule card_Diff_subset_Int) (fold finter_set, rule finite_fset)
 
 
 ML {*
--- a/src/Pure/unify.ML	Wed Jun 30 18:03:34 2010 +0200
+++ b/src/Pure/unify.ML	Wed Jun 30 18:19:53 2010 +0200
@@ -67,7 +67,7 @@
   let
     val tyenv = Envir.type_env env;
     fun bTs (Type ("fun", [T, U])) = T :: bTs U
-      | bTs (T as TVar v) =
+      | bTs (TVar v) =
           (case Type.lookup tyenv v of
             NONE => []
           | SOME T' => bTs T')
@@ -106,33 +106,37 @@
   the occurs check must ignore the types of variables. This avoids
   that ?x::?'a is unified with f(?x::T), which may lead to a cyclic
   substitution when ?'a is instantiated with T later. *)
-fun occurs_terms (seen: (indexname list) Unsynchronized.ref,
+fun occurs_terms (seen: indexname list Unsynchronized.ref,
       env: Envir.env, v: indexname, ts: term list): bool =
-  let fun occurs [] = false
-  | occurs (t::ts) =  occur t  orelse  occurs ts
-      and occur (Const _)  = false
-  | occur (Bound _)  = false
-  | occur (Free _)  = false
-  | occur (Var (w, T))  =
-      if member (op =) (!seen) w then false
-      else if Term.eq_ix (v, w) then true
-        (*no need to lookup: v has no assignment*)
-      else (seen := w:: !seen;
-            case Envir.lookup (env, (w, T)) of
-          NONE    => false
-        | SOME t => occur t)
-  | occur (Abs(_,_,body)) = occur body
-  | occur (f$t) = occur t  orelse   occur f
-  in  occurs ts  end;
-
+  let
+    fun occurs [] = false
+      | occurs (t :: ts) = occur t orelse occurs ts
+    and occur (Const _) = false
+      | occur (Bound _) = false
+      | occur (Free _) = false
+      | occur (Var (w, T)) =
+          if member (op =) (!seen) w then false
+          else if Term.eq_ix (v, w) then true
+            (*no need to lookup: v has no assignment*)
+          else
+            (seen := w :: !seen;
+             case Envir.lookup (env, (w, T)) of
+               NONE => false
+             | SOME t => occur t)
+      | occur (Abs (_, _, body)) = occur body
+      | occur (f $ t) = occur t orelse occur f;
+  in occurs ts end;
 
 
 (* f(a1,...,an)  ---->   (f,  [a1,...,an])  using the assignments*)
-fun head_of_in (env,t) : term = case t of
-    f$_ => head_of_in(env,f)
-  | Var vT => (case Envir.lookup (env, vT) of
-      SOME u => head_of_in(env,u)  |  NONE   => t)
-  | _ => t;
+fun head_of_in (env, t) : term =
+  (case t of
+    f $ _ => head_of_in (env, f)
+  | Var vT =>
+      (case Envir.lookup (env, vT) of
+        SOME u => head_of_in (env, u)
+      | NONE => t)
+  | _ => t);
 
 
 datatype occ = NoOcc | Nonrigid | Rigid;
@@ -160,42 +164,45 @@
 Warning: finds a rigid occurrence of ?f in ?f(t).
   Should NOT be called in this case: there is a flex-flex unifier
 *)
-fun rigid_occurs_term (seen: (indexname list) Unsynchronized.ref, env, v: indexname, t) =
-  let fun nonrigid t = if occurs_terms(seen,env,v,[t]) then Nonrigid
-           else NoOcc
-      fun occurs [] = NoOcc
-  | occurs (t::ts) =
-            (case occur t of
-               Rigid => Rigid
-             | oc =>  (case occurs ts of NoOcc => oc  |  oc2 => oc2))
-      and occomb (f$t) =
-            (case occur t of
-               Rigid => Rigid
-             | oc =>  (case occomb f of NoOcc => oc  |  oc2 => oc2))
-        | occomb t = occur t
-      and occur (Const _)  = NoOcc
-  | occur (Bound _)  = NoOcc
-  | occur (Free _)  = NoOcc
-  | occur (Var (w, T))  =
-      if member (op =) (!seen) w then NoOcc
-      else if Term.eq_ix (v, w) then Rigid
-      else (seen := w:: !seen;
-            case Envir.lookup (env, (w, T)) of
-          NONE    => NoOcc
-        | SOME t => occur t)
-  | occur (Abs(_,_,body)) = occur body
-  | occur (t as f$_) =  (*switch to nonrigid search?*)
-     (case head_of_in (env,f) of
-        Var (w,_) => (*w is not assigned*)
-    if Term.eq_ix (v, w) then Rigid
-    else  nonrigid t
-      | Abs(_,_,body) => nonrigid t (*not in normal form*)
-      | _ => occomb t)
-  in  occur t  end;
+fun rigid_occurs_term (seen: indexname list Unsynchronized.ref, env, v: indexname, t) =
+  let
+    fun nonrigid t =
+      if occurs_terms (seen, env, v, [t]) then Nonrigid
+      else NoOcc
+    fun occurs [] = NoOcc
+      | occurs (t :: ts) =
+          (case occur t of
+            Rigid => Rigid
+          | oc => (case occurs ts of NoOcc => oc | oc2 => oc2))
+    and occomb (f $ t) =
+        (case occur t of
+          Rigid => Rigid
+        | oc => (case occomb f of NoOcc => oc | oc2 => oc2))
+      | occomb t = occur t
+    and occur (Const _) = NoOcc
+      | occur (Bound _) = NoOcc
+      | occur (Free _) = NoOcc
+      | occur (Var (w, T)) =
+          if member (op =) (!seen) w then NoOcc
+          else if Term.eq_ix (v, w) then Rigid
+          else
+            (seen := w :: !seen;
+             case Envir.lookup (env, (w, T)) of
+               NONE => NoOcc
+             | SOME t => occur t)
+      | occur (Abs (_, _, body)) = occur body
+      | occur (t as f $ _) =  (*switch to nonrigid search?*)
+          (case head_of_in (env, f) of
+            Var (w,_) => (*w is not assigned*)
+              if Term.eq_ix (v, w) then Rigid
+              else nonrigid t
+          | Abs _ => nonrigid t (*not in normal form*)
+          | _ => occomb t)
+  in occur t end;
 
 
 exception CANTUNIFY;  (*Signals non-unifiability.  Does not signal errors!*)
-exception ASSIGN; (*Raised if not an assignment*)
+exception ASSIGN;  (*Raised if not an assignment*)
 
 
 fun unify_types thy (T, U, env) =
@@ -207,21 +214,20 @@
     in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end
     handle Type.TUNIFY => raise CANTUNIFY;
 
-fun test_unify_types thy (args as (T,U,_)) =
-let val str_of = Syntax.string_of_typ_global thy;
-    fun warn() = tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T);
-    val env' = unify_types thy args
-in if is_TVar(T) orelse is_TVar(U) then warn() else ();
-   env'
-end;
+fun test_unify_types thy (args as (T, U, _)) =
+  let
+    val str_of = Syntax.string_of_typ_global thy;
+    fun warn () = tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T);
+    val env' = unify_types thy args;
+  in if is_TVar T orelse is_TVar U then warn () else (); env' end;
 
 (*Is the term eta-convertible to a single variable with the given rbinder?
   Examples: ?a   ?f(B.0)   ?g(B.1,B.0)
   Result is var a for use in SIMPL. *)
-fun get_eta_var ([], _, Var vT)  =  vT
+fun get_eta_var ([], _, Var vT) = vT
   | get_eta_var (_::rbinder, n, f $ Bound i) =
-  if  n=i  then  get_eta_var (rbinder, n+1, f)
-     else  raise ASSIGN
+      if n = i then get_eta_var (rbinder, n + 1, f)
+      else raise ASSIGN
   | get_eta_var _ = raise ASSIGN;
 
 
@@ -229,14 +235,14 @@
   If v occurs rigidly then nonunifiable.
   If v occurs nonrigidly then must use full algorithm. *)
 fun assignment thy (env, rbinder, t, u) =
-    let val vT as (v,T) = get_eta_var (rbinder, 0, t)
-    in  case rigid_occurs_term (Unsynchronized.ref [], env, v, u) of
-        NoOcc => let val env = unify_types thy (body_type env T,
-             fastype env (rbinder,u),env)
-    in Envir.update ((vT, Logic.rlist_abs (rbinder, u)), env) end
-      | Nonrigid =>  raise ASSIGN
-      | Rigid =>  raise CANTUNIFY
-    end;
+  let val vT as (v,T) = get_eta_var (rbinder, 0, t) in
+    (case rigid_occurs_term (Unsynchronized.ref [], env, v, u) of
+      NoOcc =>
+        let val env = unify_types thy (body_type env T, fastype env (rbinder, u), env)
+        in Envir.update ((vT, Logic.rlist_abs (rbinder, u)), env) end
+    | Nonrigid => raise ASSIGN
+    | Rigid => raise CANTUNIFY)
+  end;
 
 
 (*Extends an rbinder with a new disagreement pair, if both are abstractions.
@@ -244,19 +250,20 @@
   Checks that binders have same length, since terms should be eta-normal;
     if not, raises TERM, probably indicating type mismatch.
   Uses variable a (unless the null string) to preserve user's naming.*)
-fun new_dpair thy (rbinder, Abs(a,T,body1), Abs(b,U,body2), env) =
-  let val env' = unify_types thy (T,U,env)
-      val c = if a="" then b else a
-  in new_dpair thy ((c,T) :: rbinder, body1, body2, env') end
-    | new_dpair _ (_, Abs _, _, _) = raise TERM ("new_dpair", [])
-    | new_dpair _ (_, _, Abs _, _) = raise TERM ("new_dpair", [])
-    | new_dpair _ (rbinder, t1, t2, env) = ((rbinder, t1, t2), env);
+fun new_dpair thy (rbinder, Abs (a, T, body1), Abs (b, U, body2), env) =
+      let
+        val env' = unify_types thy (T, U, env);
+        val c = if a = "" then b else a;
+      in new_dpair thy ((c,T) :: rbinder, body1, body2, env') end
+  | new_dpair _ (_, Abs _, _, _) = raise TERM ("new_dpair", [])
+  | new_dpair _ (_, _, Abs _, _) = raise TERM ("new_dpair", [])
+  | new_dpair _ (rbinder, t1, t2, env) = ((rbinder, t1, t2), env);
 
 
-fun head_norm_dpair thy (env, (rbinder,t,u)) : dpair * Envir.env =
-     new_dpair thy (rbinder,
+fun head_norm_dpair thy (env, (rbinder, t, u)) : dpair * Envir.env =
+  new_dpair thy (rbinder,
     eta_norm env (rbinder, Envir.head_norm env t),
-      eta_norm env (rbinder, Envir.head_norm env u), env);
+    eta_norm env (rbinder, Envir.head_norm env u), env);
 
 
 
@@ -266,55 +273,57 @@
   Does not even identify Vars in dpairs such as ?a =?= ?b; an attempt to
     do so caused numerous problems with no compensating advantage.
 *)
-fun SIMPL0 thy (dp0, (env,flexflex,flexrigid))
-  : Envir.env * dpair list * dpair list =
-    let val (dp as (rbinder,t,u), env) = head_norm_dpair thy (env,dp0);
-      fun SIMRANDS(f$t, g$u, env) =
-      SIMPL0 thy ((rbinder,t,u), SIMRANDS(f,g,env))
-        | SIMRANDS (t as _$_, _, _) =
-    raise TERM ("SIMPL: operands mismatch", [t,u])
-        | SIMRANDS (t, u as _$_, _) =
-    raise TERM ("SIMPL: operands mismatch", [t,u])
-        | SIMRANDS(_,_,env) = (env,flexflex,flexrigid);
-    in case (head_of t, head_of u) of
-       (Var(_,T), Var(_,U)) =>
-      let val T' = body_type env T and U' = body_type env U;
-    val env = unify_types thy (T',U',env)
-      in (env, dp::flexflex, flexrigid) end
-     | (Var _, _) =>
-      ((assignment thy (env,rbinder,t,u), flexflex, flexrigid)
-       handle ASSIGN => (env, flexflex, dp::flexrigid))
-     | (_, Var _) =>
-      ((assignment thy (env,rbinder,u,t), flexflex, flexrigid)
-       handle ASSIGN => (env, flexflex, (rbinder,u,t)::flexrigid))
-     | (Const(a,T), Const(b,U)) =>
-      if a=b then SIMRANDS(t,u, unify_types thy (T,U,env))
-      else raise CANTUNIFY
-     | (Bound i,    Bound j)    =>
-      if i=j  then SIMRANDS(t,u,env) else raise CANTUNIFY
-     | (Free(a,T),  Free(b,U))  =>
-      if a=b then SIMRANDS(t,u, unify_types thy (T,U,env))
-      else raise CANTUNIFY
-     | _ => raise CANTUNIFY
-    end;
+fun SIMPL0 thy (dp0, (env,flexflex,flexrigid)) : Envir.env * dpair list * dpair list =
+  let
+    val (dp as (rbinder, t, u), env) = head_norm_dpair thy (env, dp0);
+    fun SIMRANDS (f $ t, g $ u, env) =
+          SIMPL0 thy ((rbinder, t, u), SIMRANDS (f, g, env))
+      | SIMRANDS (t as _$_, _, _) =
+          raise TERM ("SIMPL: operands mismatch", [t, u])
+      | SIMRANDS (t, u as _ $ _, _) =
+          raise TERM ("SIMPL: operands mismatch", [t, u])
+      | SIMRANDS (_, _, env) = (env, flexflex, flexrigid);
+  in
+    (case (head_of t, head_of u) of
+      (Var (_, T), Var (_, U)) =>
+        let
+          val T' = body_type env T and U' = body_type env U;
+          val env = unify_types thy (T', U', env);
+        in (env, dp :: flexflex, flexrigid) end
+    | (Var _, _) =>
+        ((assignment thy (env, rbinder,t,u), flexflex, flexrigid)
+          handle ASSIGN => (env, flexflex, dp :: flexrigid))
+    | (_, Var _) =>
+        ((assignment thy (env, rbinder, u, t), flexflex, flexrigid)
+          handle ASSIGN => (env, flexflex, (rbinder, u, t) :: flexrigid))
+    | (Const (a, T), Const (b, U)) =>
+        if a = b then SIMRANDS (t, u, unify_types thy (T, U, env))
+        else raise CANTUNIFY
+    | (Bound i, Bound j) =>
+        if i = j then SIMRANDS (t, u, env) else raise CANTUNIFY
+    | (Free (a, T), Free (b, U)) =>
+        if a = b then SIMRANDS (t, u, unify_types thy (T, U, env))
+        else raise CANTUNIFY
+    | _ => raise CANTUNIFY)
+  end;
 
 
 (* changed(env,t) checks whether the head of t is a variable assigned in env*)
-fun changed (env, f$_) = changed (env,f)
-  | changed (env, Var v) =
-      (case Envir.lookup(env,v) of NONE=>false  |  _ => true)
+fun changed (env, f $ _) = changed (env, f)
+  | changed (env, Var v) = (case Envir.lookup (env, v) of NONE => false | _ => true)
   | changed _ = false;
 
 
 (*Recursion needed if any of the 'head variables' have been updated
   Clever would be to re-do just the affected dpairs*)
 fun SIMPL thy (env,dpairs) : Envir.env * dpair list * dpair list =
-    let val all as (env',flexflex,flexrigid) =
-      List.foldr (SIMPL0 thy) (env,[],[]) dpairs;
-  val dps = flexrigid@flexflex
-    in if exists (fn ((_,t,u)) => changed(env',t) orelse changed(env',u)) dps
-       then SIMPL thy (env',dps) else all
-    end;
+  let
+    val all as (env', flexflex, flexrigid) = List.foldr (SIMPL0 thy) (env, [], []) dpairs;
+    val dps = flexrigid @ flexflex;
+  in
+    if exists (fn (_, t, u) => changed (env', t) orelse changed (env', u)) dps
+    then SIMPL thy (env', dps) else all
+  end;
 
 
 (*Makes the terms E1,...,Em,    where Ts = [T...Tm].
@@ -322,19 +331,20 @@
   The B.j are bound vars of binder.
   The terms are not made in eta-normal-form, SIMPL does that later.
   If done here, eta-expansion must be recursive in the arguments! *)
-fun make_args name (binder: typ list, env, []) = (env, [])   (*frequent case*)
+fun make_args _ (_, env, []) = (env, [])   (*frequent case*)
   | make_args name (binder: typ list, env, Ts) : Envir.env * term list =
-       let fun funtype T = binder--->T;
-     val (env', vars) = Envir.genvars name (env, map funtype Ts)
-       in  (env',  map (fn var=> Logic.combound(var, 0, length binder)) vars)  end;
+      let
+        fun funtype T = binder ---> T;
+        val (env', vars) = Envir.genvars name (env, map funtype Ts);
+      in (env', map (fn var => Logic.combound (var, 0, length binder)) vars) end;
 
 
 (*Abstraction over a list of types, like list_abs*)
-fun types_abs ([],u) = u
-  | types_abs (T::Ts, u) = Abs("", T, types_abs(Ts,u));
+fun types_abs ([], u) = u
+  | types_abs (T :: Ts, u) = Abs ("", T, types_abs (Ts, u));
 
 (*Abstraction over the binder of a type*)
-fun type_abs (env,T,t) = types_abs(binder_types env T, t);
+fun type_abs (env, T, t) = types_abs (binder_types env T, t);
 
 
 (*MATCH taking "big steps".
@@ -346,79 +356,84 @@
   For example, projection in ?b'(?a) may be wrong if other dpairs constrain ?a.
   The order for trying projections is crucial in ?b'(?a)
   NB "vname" is only used in the call to make_args!!   *)
-fun matchcopy thy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs))
-  : (term * (Envir.env * dpair list))Seq.seq =
-let
-  val trace_tps = Config.get_global thy trace_types;
-  (*Produce copies of uarg and cons them in front of uargs*)
-  fun copycons uarg (uargs, (env, dpairs)) =
-  Seq.map(fn (uarg', ed') => (uarg'::uargs, ed'))
-      (mc (rbinder, targs,eta_norm env (rbinder, Envir.head_norm env uarg),
-     (env, dpairs)));
-  (*Produce sequence of all possible ways of copying the arg list*)
-    fun copyargs [] = Seq.cons ([],ed) Seq.empty
-      | copyargs (uarg::uargs) = Seq.maps (copycons uarg) (copyargs uargs);
-    val (uhead,uargs) = strip_comb u;
-    val base = body_type env (fastype env (rbinder,uhead));
-    fun joinargs (uargs',ed') = (list_comb(uhead,uargs'), ed');
-    (*attempt projection on argument with given typ*)
-    val Ts = map (curry (fastype env) rbinder) targs;
-    fun projenv (head, (Us,bary), targ, tail) =
-  let val env = if trace_tps then test_unify_types thy (base,bary,env)
-          else unify_types thy (base,bary,env)
-  in Seq.make (fn () =>
-      let val (env',args) = make_args vname (Ts,env,Us);
-    (*higher-order projection: plug in targs for bound vars*)
-    fun plugin arg = list_comb(head_of arg, targs);
-    val dp = (rbinder, list_comb(targ, map plugin args), u);
-    val (env2,frigid,fflex) = SIMPL thy (env', dp::dpairs)
-        (*may raise exception CANTUNIFY*)
-      in  SOME ((list_comb(head,args), (env2, frigid@fflex)),
-      tail)
-      end  handle CANTUNIFY => Seq.pull tail)
-  end handle CANTUNIFY => tail;
-    (*make a list of projections*)
-    fun make_projs (T::Ts, targ::targs) =
-        (Bound(length Ts), T, targ) :: make_projs (Ts,targs)
-      | make_projs ([],[]) = []
-      | make_projs _ = raise TERM ("make_projs", u::targs);
-    (*try projections and imitation*)
-    fun matchfun ((bvar,T,targ)::projs) =
-         (projenv(bvar, strip_type env T, targ, matchfun projs))
-      | matchfun [] = (*imitation last of all*)
-        (case uhead of
-     Const _ => Seq.map joinargs (copyargs uargs)
-         | Free _  => Seq.map joinargs (copyargs uargs)
-         | _ => Seq.empty)  (*if Var, would be a loop!*)
-in case uhead of
-  Abs(a, T, body) =>
-      Seq.map(fn (body', ed') => (Abs (a,T,body'), ed'))
-    (mc ((a,T)::rbinder,
-      (map (incr_boundvars 1) targs) @ [Bound 0], body, ed))
-      | Var (w,uary) =>
-      (*a flex-flex dpair: make variable for t*)
-      let val (env', newhd) = Envir.genvar (#1 w) (env, Ts---> base)
-    val tabs = Logic.combound(newhd, 0, length Ts)
-    val tsub = list_comb(newhd,targs)
-      in  Seq.single (tabs, (env', (rbinder,tsub,u):: dpairs))
-      end
-      | _ =>  matchfun(rev(make_projs(Ts, targs)))
-end
-in mc end;
+fun matchcopy thy vname =
+  let
+    fun mc (rbinder, targs, u, ed as (env, dpairs)) : (term * (Envir.env * dpair list)) Seq.seq =
+      let
+        val trace_tps = Config.get_global thy trace_types;
+        (*Produce copies of uarg and cons them in front of uargs*)
+        fun copycons uarg (uargs, (env, dpairs)) =
+          Seq.map (fn (uarg', ed') => (uarg' :: uargs, ed'))
+            (mc (rbinder, targs,eta_norm env (rbinder, Envir.head_norm env uarg),
+              (env, dpairs)));
+        (*Produce sequence of all possible ways of copying the arg list*)
+        fun copyargs [] = Seq.cons ([], ed) Seq.empty
+          | copyargs (uarg :: uargs) = Seq.maps (copycons uarg) (copyargs uargs);
+        val (uhead, uargs) = strip_comb u;
+        val base = body_type env (fastype env (rbinder, uhead));
+        fun joinargs (uargs', ed') = (list_comb (uhead, uargs'), ed');
+        (*attempt projection on argument with given typ*)
+        val Ts = map (curry (fastype env) rbinder) targs;
+        fun projenv (head, (Us, bary), targ, tail) =
+          let
+            val env =
+              if trace_tps then test_unify_types thy (base, bary, env)
+              else unify_types thy (base, bary, env)
+          in
+            Seq.make (fn () =>
+              let
+                val (env', args) = make_args vname (Ts, env, Us);
+                (*higher-order projection: plug in targs for bound vars*)
+                fun plugin arg = list_comb (head_of arg, targs);
+                val dp = (rbinder, list_comb (targ, map plugin args), u);
+                val (env2, frigid, fflex) = SIMPL thy (env', dp :: dpairs);
+                (*may raise exception CANTUNIFY*)
+              in
+                SOME ((list_comb (head, args), (env2, frigid @ fflex)), tail)
+              end handle CANTUNIFY => Seq.pull tail)
+          end handle CANTUNIFY => tail;
+        (*make a list of projections*)
+        fun make_projs (T::Ts, targ::targs) =
+            (Bound(length Ts), T, targ) :: make_projs (Ts,targs)
+          | make_projs ([],[]) = []
+          | make_projs _ = raise TERM ("make_projs", u::targs);
+        (*try projections and imitation*)
+        fun matchfun ((bvar,T,targ)::projs) =
+             (projenv(bvar, strip_type env T, targ, matchfun projs))
+          | matchfun [] = (*imitation last of all*)
+            (case uhead of
+         Const _ => Seq.map joinargs (copyargs uargs)
+             | Free _  => Seq.map joinargs (copyargs uargs)
+             | _ => Seq.empty)  (*if Var, would be a loop!*)
+    in
+      (case uhead of
+        Abs (a, T, body) =>
+          Seq.map (fn (body', ed') => (Abs (a, T, body'), ed'))
+            (mc ((a, T) :: rbinder, (map (incr_boundvars 1) targs) @ [Bound 0], body, ed))
+      | Var (w, _) =>
+          (*a flex-flex dpair: make variable for t*)
+          let
+            val (env', newhd) = Envir.genvar (#1 w) (env, Ts ---> base);
+            val tabs = Logic.combound (newhd, 0, length Ts);
+            val tsub = list_comb (newhd, targs);
+          in Seq.single (tabs, (env', (rbinder, tsub, u) :: dpairs)) end
+      | _ => matchfun (rev (make_projs (Ts, targs))))
+    end;
+  in mc end;
 
 
 (*Call matchcopy to produce assignments to the variable in the dpair*)
-fun MATCH thy (env, (rbinder,t,u), dpairs)
-  : (Envir.env * dpair list)Seq.seq =
-  let val (Var (vT as (v, T)), targs) = strip_comb t;
-      val Ts = binder_types env T;
-      fun new_dset (u', (env',dpairs')) =
-    (*if v was updated to s, must unify s with u' *)
-    case Envir.lookup (env', vT) of
-        NONE => (Envir.update ((vT, types_abs(Ts, u')), env'),  dpairs')
-      | SOME s => (env', ([], s, types_abs(Ts, u'))::dpairs')
-  in Seq.map new_dset
-         (matchcopy thy (#1 v) (rbinder, targs, u, (env,dpairs)))
+fun MATCH thy (env, (rbinder, t, u), dpairs) : (Envir.env * dpair list) Seq.seq =
+  let
+    val (Var (vT as (v, T)), targs) = strip_comb t;
+    val Ts = binder_types env T;
+    fun new_dset (u', (env', dpairs')) =
+      (*if v was updated to s, must unify s with u' *)
+      (case Envir.lookup (env', vT) of
+        NONE => (Envir.update ((vT, types_abs (Ts, u')), env'), dpairs')
+      | SOME s => (env', ([], s, types_abs (Ts, u')) :: dpairs'));
+  in
+    Seq.map new_dset (matchcopy thy (#1 v) (rbinder, targs, u, (env, dpairs)))
   end;
 
 
@@ -428,23 +443,21 @@
 (*At end of unification, do flex-flex assignments like ?a -> ?f(?b)
   Attempts to update t with u, raising ASSIGN if impossible*)
 fun ff_assign thy (env, rbinder, t, u) : Envir.env =
-let val vT as (v,T) = get_eta_var(rbinder,0,t)
-in if occurs_terms (Unsynchronized.ref [], env, v, [u]) then raise ASSIGN
-   else let val env = unify_types thy (body_type env T,
-          fastype env (rbinder,u),
-          env)
-  in Envir.vupdate ((vT, Logic.rlist_abs (rbinder, u)), env) end
-end;
+  let val vT as (v, T) = get_eta_var (rbinder, 0, t) in
+    if occurs_terms (Unsynchronized.ref [], env, v, [u]) then raise ASSIGN
+    else
+      let val env = unify_types thy (body_type env T, fastype env (rbinder, u), env)
+      in Envir.vupdate ((vT, Logic.rlist_abs (rbinder, u)), env) end
+  end;
 
 
 (*Flex argument: a term, its type, and the index that refers to it.*)
-type flarg = {t: term,  T: typ,  j: int};
-
+type flarg = {t: term, T: typ, j: int};
 
 (*Form the arguments into records for deletion/sorting.*)
-fun flexargs ([],[],[]) = [] : flarg list
-  | flexargs (j::js, t::ts, T::Ts) = {j=j, t=t, T=T} :: flexargs(js,ts,Ts)
-  | flexargs _ = error"flexargs";
+fun flexargs ([], [], []) = [] : flarg list
+  | flexargs (j :: js, t :: ts, T :: Ts) = {j = j, t = t, T = T} :: flexargs (js, ts, Ts)
+  | flexargs _ = raise Fail "flexargs";
 
 
 (*If an argument contains a banned Bound, then it should be deleted.
@@ -455,173 +468,181 @@
 
 (*Check whether the 'banned' bound var indices occur rigidly in t*)
 fun rigid_bound (lev, banned) t =
-  let val (head,args) = strip_comb t
-  in
-      case head of
-    Bound i => member (op =) banned (i-lev)  orelse
-               exists (rigid_bound (lev, banned)) args
-  | Var _ => false  (*no rigid occurrences here!*)
-  | Abs (_,_,u) =>
-         rigid_bound(lev+1, banned) u  orelse
-         exists (rigid_bound (lev, banned)) args
-  | _ => exists (rigid_bound (lev, banned)) args
+  let val (head,args) = strip_comb t in
+    (case head of
+      Bound i =>
+        member (op =) banned (i - lev) orelse exists (rigid_bound (lev, banned)) args
+    | Var _ => false  (*no rigid occurrences here!*)
+    | Abs (_, _, u) =>
+        rigid_bound (lev + 1, banned) u orelse
+        exists (rigid_bound (lev, banned)) args
+    | _ => exists (rigid_bound (lev, banned)) args)
   end;
 
 (*Squash down indices at level >=lev to delete the banned from a term.*)
 fun change_bnos banned =
-  let fun change lev (Bound i) =
-      if i<lev then Bound i
-      else  if member (op =) banned (i-lev)
-      then raise CHANGE_FAIL (**flexible occurrence: give up**)
-      else  Bound (i - length (filter (fn j => j < i-lev) banned))
-  | change lev (Abs (a,T,t)) = Abs (a, T, change(lev+1) t)
-  | change lev (t$u) = change lev t $ change lev u
-  | change lev t = t
-  in  change 0  end;
+  let
+    fun change lev (Bound i) =
+          if i < lev then Bound i
+          else if member (op =) banned (i - lev) then
+            raise CHANGE_FAIL (**flexible occurrence: give up**)
+          else Bound (i - length (filter (fn j => j < i - lev) banned))
+      | change lev (Abs (a, T, t)) = Abs (a, T, change(lev + 1) t)
+      | change lev (t $ u) = change lev t $ change lev u
+      | change lev t = t;
+  in change 0 end;
 
 (*Change indices, delete the argument if it contains a banned Bound*)
-fun change_arg banned ({j,t,T}, args) : flarg list =
-    if rigid_bound (0, banned) t  then  args  (*delete argument!*)
-    else  {j=j, t= change_bnos banned t, T=T} :: args;
+fun change_arg banned ({j, t, T}, args) : flarg list =
+  if rigid_bound (0, banned) t then args  (*delete argument!*)
+  else {j = j, t = change_bnos banned t, T = T} :: args;
 
 
 (*Sort the arguments to create assignments if possible:
   create eta-terms like ?g(B.1,B.0) *)
-fun arg_less ({t= Bound i1,...}, {t= Bound i2,...}) = (i2<i1)
-  | arg_less (_:flarg, _:flarg) = false;
+fun arg_less ({t = Bound i1, ...}, {t = Bound i2, ...}) = (i2 < i1)
+  | arg_less (_: flarg, _: flarg) = false;
 
 (*Test whether the new term would be eta-equivalent to a variable --
   if so then there is no point in creating a new variable*)
-fun decreasing n ([]: flarg list) = (n=0)
-  | decreasing n ({j,...}::args) = j=n-1 andalso decreasing (n-1) args;
+fun decreasing n ([]: flarg list) = (n = 0)
+  | decreasing n ({j, ...} :: args) = j = n - 1 andalso decreasing (n - 1) args;
 
 (*Delete banned indices in the term, simplifying it.
   Force an assignment, if possible, by sorting the arguments.
   Update its head; squash indices in arguments. *)
 fun clean_term banned (env,t) =
-    let val (Var(v,T), ts) = strip_comb t
-  val (Ts,U) = strip_type env T
-  and js = length ts - 1  downto 0
-  val args = sort (make_ord arg_less)
-    (List.foldr (change_arg banned) [] (flexargs (js,ts,Ts)))
-  val ts' = map (#t) args
-    in
-    if decreasing (length Ts) args then (env, (list_comb(Var(v,T), ts')))
-    else let val (env',v') = Envir.genvar (#1v) (env, map (#T) args ---> U)
-       val body = list_comb(v', map (Bound o #j) args)
-       val env2 = Envir.vupdate ((((v, T), types_abs(Ts, body)),   env'))
-       (*the vupdate affects ts' if they contain v*)
-   in
-       (env2, Envir.norm_term env2 (list_comb(v',ts')))
-         end
-    end;
+  let
+    val (Var (v, T), ts) = strip_comb t;
+    val (Ts, U) = strip_type env T
+    and js = length ts - 1  downto 0;
+    val args = sort (make_ord arg_less) (List.foldr (change_arg banned) [] (flexargs (js, ts, Ts)))
+    val ts' = map #t args;
+  in
+    if decreasing (length Ts) args then (env, (list_comb (Var (v, T), ts')))
+    else
+      let
+        val (env', v') = Envir.genvar (#1 v) (env, map #T args ---> U);
+        val body = list_comb (v', map (Bound o #j) args);
+        val env2 = Envir.vupdate ((((v, T), types_abs (Ts, body)), env'));
+        (*the vupdate affects ts' if they contain v*)
+      in (env2, Envir.norm_term env2 (list_comb (v', ts'))) end
+  end;
 
 
 (*Add tpair if not trivial or already there.
   Should check for swapped pairs??*)
-fun add_tpair (rbinder, (t0,u0), tpairs) : (term*term) list =
+fun add_tpair (rbinder, (t0, u0), tpairs) : (term * term) list =
   if t0 aconv u0 then tpairs
   else
-  let val t = Logic.rlist_abs(rbinder, t0)  and  u = Logic.rlist_abs(rbinder, u0);
-      fun same(t',u') = (t aconv t') andalso (u aconv u')
-  in  if exists same tpairs  then tpairs  else (t,u)::tpairs  end;
+    let
+      val t = Logic.rlist_abs (rbinder, t0)
+      and u = Logic.rlist_abs (rbinder, u0);
+      fun same (t', u') = (t aconv t') andalso (u aconv u')
+    in if exists same tpairs then tpairs else (t, u) :: tpairs end;
 
 
 (*Simplify both terms and check for assignments.
   Bound vars in the binder are "banned" unless used in both t AND u *)
-fun clean_ffpair thy ((rbinder, t, u), (env,tpairs)) =
-  let val loot = loose_bnos t  and  loou = loose_bnos u
-      fun add_index (j, (a,T)) (bnos, newbinder) =
-            if  member (op =) loot j  andalso  member (op =) loou j
-            then  (bnos, (a,T)::newbinder)  (*needed by both: keep*)
-            else  (j::bnos, newbinder);   (*remove*)
-      val (banned,rbin') = fold_rev add_index
-        ((0 upto (length rbinder - 1)) ~~ rbinder) ([],[]);
-      val (env', t') = clean_term banned (env, t);
-      val (env'',u') = clean_term banned (env',u)
-  in  (ff_assign thy (env'', rbin', t', u'), tpairs)
-      handle ASSIGN => (ff_assign thy (env'', rbin', u', t'), tpairs)
-      handle ASSIGN => (env'', add_tpair(rbin', (t',u'), tpairs))
+fun clean_ffpair thy ((rbinder, t, u), (env, tpairs)) =
+  let
+    val loot = loose_bnos t and loou = loose_bnos u
+    fun add_index (j, (a, T)) (bnos, newbinder) =
+      if member (op =) loot j andalso member (op =) loou j
+      then (bnos, (a, T) :: newbinder)  (*needed by both: keep*)
+      else (j :: bnos, newbinder);   (*remove*)
+    val (banned, rbin') = fold_rev add_index ((0 upto (length rbinder - 1)) ~~ rbinder) ([], []);
+    val (env', t') = clean_term banned (env, t);
+    val (env'',u') = clean_term banned (env',u);
+  in
+    (ff_assign thy (env'', rbin', t', u'), tpairs)
+      handle ASSIGN =>
+        (ff_assign thy (env'', rbin', u', t'), tpairs)
+          handle ASSIGN => (env'', add_tpair (rbin', (t', u'), tpairs))
   end
-  handle CHANGE_FAIL => (env, add_tpair(rbinder, (t,u), tpairs));
+  handle CHANGE_FAIL => (env, add_tpair (rbinder, (t, u), tpairs));
 
 
 (*IF the flex-flex dpair is an assignment THEN do it  ELSE  put in tpairs
   eliminates trivial tpairs like t=t, as well as repeated ones
   trivial tpairs can easily escape SIMPL:  ?A=t, ?A=?B, ?B=t gives t=t
   Resulting tpairs MAY NOT be in normal form:  assignments may occur here.*)
-fun add_ffpair thy ((rbinder,t0,u0), (env,tpairs))
-      : Envir.env * (term*term)list =
-  let val t = Envir.norm_term env t0  and  u = Envir.norm_term env u0
-  in  case  (head_of t, head_of u) of
-      (Var(v,T), Var(w,U)) =>  (*Check for identical variables...*)
-  if Term.eq_ix (v, w) then     (*...occur check would falsely return true!*)
-      if T=U then (env, add_tpair (rbinder, (t,u), tpairs))
-      else raise TERM ("add_ffpair: Var name confusion", [t,u])
-  else if Term_Ord.indexname_ord (v, w) = LESS then (*prefer to update the LARGER variable*)
-       clean_ffpair thy ((rbinder, u, t), (env,tpairs))
-        else clean_ffpair thy ((rbinder, t, u), (env,tpairs))
-    | _ => raise TERM ("add_ffpair: Vars expected", [t,u])
+fun add_ffpair thy ((rbinder,t0,u0), (env,tpairs)) : Envir.env * (term * term) list =
+  let
+    val t = Envir.norm_term env t0
+    and u = Envir.norm_term env u0;
+  in
+    (case (head_of t, head_of u) of
+      (Var (v, T), Var (w, U)) =>  (*Check for identical variables...*)
+        if Term.eq_ix (v, w) then     (*...occur check would falsely return true!*)
+          if T = U then (env, add_tpair (rbinder, (t, u), tpairs))
+          else raise TERM ("add_ffpair: Var name confusion", [t, u])
+        else if Term_Ord.indexname_ord (v, w) = LESS then (*prefer to update the LARGER variable*)
+          clean_ffpair thy ((rbinder, u, t), (env, tpairs))
+        else clean_ffpair thy ((rbinder, t, u), (env, tpairs))
+    | _ => raise TERM ("add_ffpair: Vars expected", [t, u]))
   end;
 
 
 (*Print a tracing message + list of dpairs.
   In t==u print u first because it may be rigid or flexible --
     t is always flexible.*)
-fun print_dpairs thy msg (env,dpairs) =
-  let fun pdp (rbinder,t,u) =
-        let fun termT t = Syntax.pretty_term_global thy
-                              (Envir.norm_term env (Logic.rlist_abs(rbinder,t)))
-            val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1,
-                          termT t];
-        in tracing(Pretty.string_of(Pretty.blk(0,bsymbs))) end;
-  in  tracing msg;  List.app pdp dpairs  end;
+fun print_dpairs thy msg (env, dpairs) =
+  let
+    fun pdp (rbinder, t, u) =
+      let
+        fun termT t =
+          Syntax.pretty_term_global thy (Envir.norm_term env (Logic.rlist_abs (rbinder, t)));
+        val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1, termT t];
+      in tracing (Pretty.string_of (Pretty.blk (0, bsymbs))) end;
+  in tracing msg; List.app pdp dpairs end;
 
 
 (*Unify the dpairs in the environment.
   Returns flex-flex disagreement pairs NOT IN normal form.
   SIMPL may raise exception CANTUNIFY. *)
-fun hounifiers (thy,env, tus : (term*term)list)
-  : (Envir.env * (term*term)list)Seq.seq =
+fun hounifiers (thy, env, tus : (term * term) list) : (Envir.env * (term * term) list) Seq.seq =
   let
     val trace_bnd = Config.get_global thy trace_bound;
     val search_bnd = Config.get_global thy search_bound;
     val trace_smp = Config.get_global thy trace_simp;
-    fun add_unify tdepth ((env,dpairs), reseq) =
-    Seq.make (fn()=>
-    let val (env',flexflex,flexrigid) =
-         (if tdepth> trace_bnd andalso trace_smp
-    then print_dpairs thy "Enter SIMPL" (env,dpairs)  else ();
-    SIMPL thy (env,dpairs))
-    in case flexrigid of
-        [] => SOME (List.foldr (add_ffpair thy) (env',[]) flexflex, reseq)
-      | dp::frigid' =>
-    if tdepth > search_bnd then
-        (warning "Unification bound exceeded"; Seq.pull reseq)
-    else
-    (if tdepth > trace_bnd then
-        print_dpairs thy "Enter MATCH" (env',flexrigid@flexflex)
-     else ();
-     Seq.pull (Seq.it_right (add_unify (tdepth+1))
-         (MATCH thy (env',dp, frigid'@flexflex), reseq)))
-    end
-    handle CANTUNIFY =>
-      (if tdepth > trace_bnd then tracing"Failure node" else ();
-       Seq.pull reseq));
-     val dps = map (fn(t,u)=> ([],t,u)) tus
+    fun add_unify tdepth ((env, dpairs), reseq) =
+      Seq.make (fn () =>
+        let
+          val (env', flexflex, flexrigid) =
+           (if tdepth > trace_bnd andalso trace_smp
+            then print_dpairs thy "Enter SIMPL" (env, dpairs) else ();
+            SIMPL thy (env, dpairs));
+        in
+          (case flexrigid of
+            [] => SOME (List.foldr (add_ffpair thy) (env', []) flexflex, reseq)
+          | dp :: frigid' =>
+              if tdepth > search_bnd then
+                (warning "Unification bound exceeded"; Seq.pull reseq)
+              else
+               (if tdepth > trace_bnd then
+                  print_dpairs thy "Enter MATCH" (env',flexrigid@flexflex)
+                else ();
+                Seq.pull (Seq.it_right
+                    (add_unify (tdepth + 1)) (MATCH thy (env',dp, frigid'@flexflex), reseq))))
+        end
+        handle CANTUNIFY =>
+         (if tdepth > trace_bnd then tracing"Failure node" else ();
+          Seq.pull reseq));
+    val dps = map (fn (t, u) => ([], t, u)) tus;
   in add_unify 1 ((env, dps), Seq.empty) end;
 
 fun unifiers (params as (thy, env, tus)) =
   Seq.cons (fold (Pattern.unify thy) tus env, []) Seq.empty
     handle Pattern.Unif => Seq.empty
-         | Pattern.Pattern => hounifiers params;
+      | Pattern.Pattern => hounifiers params;
 
 
 (*For smash_flexflex1*)
 fun var_head_of (env,t) : indexname * typ =
-  case head_of (strip_abs_body (Envir.norm_term env t)) of
-      Var(v,T) => (v,T)
-    | _ => raise CANTUNIFY;  (*not flexible, cannot use trivial substitution*)
+  (case head_of (strip_abs_body (Envir.norm_term env t)) of
+    Var (v, T) => (v, T)
+  | _ => raise CANTUNIFY);  (*not flexible, cannot use trivial substitution*)
 
 
 (*Eliminate a flex-flex pair by the trivial substitution, see Huet (1975)
@@ -631,23 +652,25 @@
   Unlike Huet (1975), does not smash together all variables of same type --
     requires more work yet gives a less general unifier (fewer variables).
   Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *)
-fun smash_flexflex1 ((t,u), env) : Envir.env =
-  let val vT as (v,T) = var_head_of (env,t)
-      and wU as (w,U) = var_head_of (env,u);
-      val (env', var) = Envir.genvar (#1v) (env, body_type env T)
-      val env'' = Envir.vupdate ((wU, type_abs (env', U, var)), env')
-  in  if vT = wU then env''  (*the other update would be identical*)
-      else Envir.vupdate ((vT, type_abs (env', T, var)), env'')
+fun smash_flexflex1 ((t, u), env) : Envir.env =
+  let
+    val vT as (v, T) = var_head_of (env, t)
+    and wU as (w, U) = var_head_of (env, u);
+    val (env', var) = Envir.genvar (#1 v) (env, body_type env T);
+    val env'' = Envir.vupdate ((wU, type_abs (env', U, var)), env');
+  in
+    if vT = wU then env''  (*the other update would be identical*)
+    else Envir.vupdate ((vT, type_abs (env', T, var)), env'')
   end;
 
 
 (*Smash all flex-flexpairs.  Should allow selection of pairs by a predicate?*)
-fun smash_flexflex (env,tpairs) : Envir.env =
+fun smash_flexflex (env, tpairs) : Envir.env =
   List.foldr smash_flexflex1 env tpairs;
 
 (*Returns unifiers with no remaining disagreement pairs*)
 fun smash_unifiers thy tus env =
-    Seq.map smash_flexflex (unifiers(thy,env,tus));
+  Seq.map smash_flexflex (unifiers (thy, env, tus));
 
 
 (*Pattern matching*)
--- a/src/Tools/Code/code_printer.ML	Wed Jun 30 18:03:34 2010 +0200
+++ b/src/Tools/Code/code_printer.ML	Wed Jun 30 18:19:53 2010 +0200
@@ -63,7 +63,7 @@
   val brackify: fixity -> Pretty.T list -> Pretty.T
   val brackify_infix: int * lrx -> fixity -> Pretty.T * Pretty.T * Pretty.T -> Pretty.T
   val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
-  val applify: string -> string -> fixity -> Pretty.T -> Pretty.T list -> Pretty.T
+  val applify: string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T
 
   type tyco_syntax
   type simple_const_syntax
@@ -230,10 +230,10 @@
     else p
   end;
 
-fun applify opn cls fxy_ctxt p [] = p
-  | applify opn cls fxy_ctxt p ps =
+fun applify opn cls f fxy_ctxt p [] = p
+  | applify opn cls f fxy_ctxt p ps =
       (if (fixity BR fxy_ctxt) then enclose "(" ")" else Pretty.block)
-        (p @@ enum "," opn cls ps);
+        (p @@ enum "," opn cls (map f ps));
 
 
 (* generic syntax *)
--- a/src/Tools/Code/code_scala.ML	Wed Jun 30 18:03:34 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Wed Jun 30 18:19:53 2010 +0200
@@ -23,17 +23,26 @@
 (** Scala serializer **)
 
 fun print_scala_stmt labelled_name syntax_tyco syntax_const reserved
-    args_num is_singleton deresolve =
+    args_num is_singleton_constr deresolve =
   let
     val deresolve_base = Long_Name.base_name o deresolve;
-    val lookup_tyvar = first_upper oo lookup_var;
-    fun print_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
-         of NONE => applify "[" "]" fxy
-              ((str o deresolve) tyco) (map (print_typ tyvars NOBR) tys)
+    fun lookup_tyvar tyvars = lookup_var tyvars o first_upper;
+    fun intro_tyvars vs = intro_vars (map (first_upper o fst) vs);
+    fun print_tyco_expr tyvars fxy (tyco, tys) = applify "[" "]"
+          (print_typ tyvars NOBR) fxy ((str o deresolve) tyco) tys
+    and print_typ tyvars fxy (tyco `%% tys) = (case syntax_tyco tyco
+         of NONE => print_tyco_expr tyvars fxy (tyco, tys)
           | SOME (i, print) => print (print_typ tyvars) fxy tys)
       | print_typ tyvars fxy (ITyVar v) = (str o lookup_tyvar tyvars) v;
-    fun print_typed tyvars p ty =
-      Pretty.block [p, str ":", Pretty.brk 1, print_typ tyvars NOBR ty]
+    fun print_dicttyp tyvars (class, ty) = print_tyco_expr tyvars NOBR (class, [ty]);
+    fun print_tupled_typ tyvars ([], ty) =
+          print_typ tyvars NOBR ty
+      | print_tupled_typ tyvars ([ty1], ty2) =
+          concat [print_typ tyvars BR ty1, str "=>", print_typ tyvars NOBR ty2]
+      | print_tupled_typ tyvars (tys, ty) =
+          concat [enum "," "(" ")" (map (print_typ tyvars NOBR) tys),
+            str "=>", print_typ tyvars NOBR ty];
+    fun constraint p1 p2 = Pretty.block [p1, str ":", Pretty.brk 1, p2];
     fun print_var vars NONE = str "_"
       | print_var vars (SOME v) = (str o lookup_var vars) v
     fun print_term tyvars is_pat some_thm vars fxy (IConst c) =
@@ -41,9 +50,8 @@
       | print_term tyvars is_pat some_thm vars fxy (t as (t1 `$ t2)) =
           (case Code_Thingol.unfold_const_app t
            of SOME app => print_app tyvars is_pat some_thm vars fxy app
-            | _ => applify "(" ")" fxy
-                (print_term tyvars is_pat some_thm vars BR t1)
-                [print_term tyvars is_pat some_thm vars NOBR t2])
+            | _ => applify "(" ")" (print_term tyvars is_pat some_thm vars NOBR) fxy
+                (print_term tyvars is_pat some_thm vars BR t1) [t2])
       | print_term tyvars is_pat some_thm vars fxy (IVar v) =
           print_var vars v
       | print_term tyvars is_pat some_thm vars fxy ((v, ty) `|=> t) =
@@ -51,7 +59,7 @@
             val vars' = intro_vars (the_list v) vars;
           in
             concat [
-              Pretty.block [str "(", print_typed tyvars (print_var vars' v) ty, str ")"],
+              enclose "(" ")" [constraint (print_var vars' v) (print_typ tyvars NOBR ty)],
               str "=>",
               print_term tyvars false some_thm vars' NOBR t
             ]
@@ -68,12 +76,12 @@
         val k = length ts;
         val l = case syntax_const c of NONE => args_num c | SOME (l, _) => l;
         val arg_typs' = if is_pat orelse
-          (is_none (syntax_const c) andalso is_singleton c) then [] else arg_typs;
+          (is_none (syntax_const c) andalso is_singleton_constr c) then [] else arg_typs;
         val (no_syntax, print') = case syntax_const c
-         of NONE => (true, fn ts => applify "(" ")" fxy
-              (applify "[" "]" NOBR ((str o deresolve) c)
-                (map (print_typ tyvars NOBR) arg_typs'))
-                  (map (print_term tyvars is_pat some_thm vars NOBR) ts))
+         of NONE => (true, fn ts => applify "(" ")"
+              (print_term tyvars is_pat some_thm vars NOBR) fxy
+                (applify "[" "]" (print_typ tyvars NOBR)
+                  NOBR ((str o deresolve) c) arg_typs') ts)
           | SOME (_, print) => (false, fn ts =>
               print (print_term tyvars is_pat some_thm) some_thm vars fxy
                 (ts ~~ take l function_typs));
@@ -94,15 +102,14 @@
             fun print_match ((pat, ty), t) vars =
               vars
               |> print_bind tyvars some_thm BR pat
-              |>> (fn p => semicolon [Pretty.block [str "val", Pretty.brk 1, p,
-                str ":", Pretty.brk 1, print_typ tyvars NOBR ty],
+              |>> (fn p => concat [str "val", constraint p (print_typ tyvars NOBR ty),
                   str "=", print_term tyvars false some_thm vars NOBR t])
-            val (ps, vars') = fold_map print_match binds vars;
-          in
-            brackify_block fxy
-              (str "{")
-              (ps @| print_term tyvars false some_thm vars' NOBR body)
-              (str "}")
+            val (all_ps, vars') = fold_map print_match binds vars;
+            val (ps, p) = split_last all_ps;
+          in brackify_block fxy
+            (str "{")
+            (ps @ Pretty.block [p, str ";"] @@ print_term tyvars false some_thm vars' NOBR body)
+            (str "}")
           end
       | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
           let
@@ -118,156 +125,124 @@
           end
       | print_case tyvars some_thm vars fxy ((_, []), _) =
           (brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"];
-    fun print_defhead tyvars vars p vs params tys implicits (*FIXME simplify*) ty =
-      Pretty.block [str "def ", print_typed tyvars (applify "(implicit " ")" NOBR
-        (applify "(" ")" NOBR
-          (applify "[" "]" NOBR p (map (fn (v, sort) =>
-              (str o implode)
-                (lookup_tyvar tyvars v :: map (prefix ": " o deresolve) sort)) vs))
-            (map2 (fn param => fn ty => print_typed tyvars
-                ((str o lookup_var vars) param) ty)
-              params tys)) implicits) ty, str " ="]
-    fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
-        (case filter (snd o snd) raw_eqs
-         of [] =>
-              let
-                val (tys, ty') = Code_Thingol.unfold_fun ty;
-                val params = Name.invents (snd reserved) "a" (length tys);
-                val tyvars = intro_vars (map fst vs) reserved;
-                val vars = intro_vars params reserved;
-              in
-                concat [print_defhead tyvars vars ((str o deresolve) name) vs params tys [] ty',
-                  str ("error(\"" ^ name ^ "\")")]
-              end
-          | eqs =>
+    fun print_context tyvars vs name = applify "[" "]"
+      (fn (v, sort) => (Pretty.block o map str)
+        (lookup_tyvar tyvars v :: maps (fn sort => [": ", deresolve sort]) sort))
+          NOBR ((str o deresolve) name) vs;
+    fun print_defhead tyvars vars name vs params tys ty =
+      Pretty.block [str "def ", constraint (applify "(" ")" (fn (param, ty) =>
+        constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty))
+          NOBR (print_context tyvars vs name) (params ~~ tys)) (print_typ tyvars NOBR ty),
+            str " ="];
+    fun print_def name (vs, ty) [] =
+          let
+            val (tys, ty') = Code_Thingol.unfold_fun ty;
+            val params = Name.invents (snd reserved) "a" (length tys);
+            val tyvars = intro_tyvars vs reserved;
+            val vars = intro_vars params reserved;
+          in
+            concat [print_defhead tyvars vars name vs params tys ty',
+              str ("error(\"" ^ name ^ "\")")]
+          end
+      | print_def name (vs, ty) eqs =
+          let
+            val tycos = fold (fn ((ts, t), _) =>
+              fold Code_Thingol.add_tyconames (t :: ts)) eqs [];
+            val tyvars = reserved
+              |> intro_base_names
+                   (is_none o syntax_tyco) deresolve tycos
+              |> intro_tyvars vs;
+            val simple = case eqs
+             of [((ts, _), _)] => forall Code_Thingol.is_IVar ts
+              | _ => false;
+            val consts = fold Code_Thingol.add_constnames
+              (map (snd o fst) eqs) [];
+            val vars1 = reserved
+              |> intro_base_names
+                   (is_none o syntax_const) deresolve consts
+            val params = if simple
+              then (map (fn IVar (SOME x) => x) o fst o fst o hd) eqs
+              else aux_params vars1 (map (fst o fst) eqs);
+            val vars2 = intro_vars params vars1;
+            val (tys', ty') = Code_Thingol.unfold_fun_n (length params) ty;
+            fun print_tuple [p] = p
+              | print_tuple ps = enum "," "(" ")" ps;
+            fun print_rhs vars' ((_, t), (some_thm, _)) =
+              print_term tyvars false some_thm vars' NOBR t;
+            fun print_clause (eq as ((ts, _), (some_thm, _))) =
               let
-                val tycos = fold (fn ((ts, t), _) =>
-                  fold Code_Thingol.add_tyconames (t :: ts)) eqs [];
-                val tyvars = reserved
-                  |> intro_base_names
-                       (is_none o syntax_tyco) deresolve tycos
-                  |> intro_vars (map fst vs);
-                val simple = case eqs
-                 of [((ts, _), _)] => forall Code_Thingol.is_IVar ts
-                  | _ => false;
-                val consts = fold Code_Thingol.add_constnames
-                  (map (snd o fst) eqs) [];
-                val vars1 = reserved
-                  |> intro_base_names
-                       (is_none o syntax_const) deresolve consts
-                val params = if simple
-                  then (map (fn IVar (SOME x) => x) o fst o fst o hd) eqs
-                  else aux_params vars1 (map (fst o fst) eqs);
-                val vars2 = intro_vars params vars1;
-                val (tys, ty1) = Code_Thingol.unfold_fun ty;
-                val (tys1, tys2) = chop (length params) tys;
-                val ty2 = Library.foldr
-                  (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (tys2, ty1);
-                fun print_tuple [p] = p
-                  | print_tuple ps = enum "," "(" ")" ps;
-                fun print_rhs vars' ((_, t), (some_thm, _)) =
-                  print_term tyvars false some_thm vars' NOBR t;
-                fun print_clause (eq as ((ts, _), (some_thm, _))) =
-                  let
-                    val vars' = intro_vars ((fold o Code_Thingol.fold_varnames)
-                      (insert (op =)) ts []) vars1;
-                  in
-                    concat [str "case",
-                      print_tuple (map (print_term tyvars true some_thm vars' NOBR) ts),
-                      str "=>", print_rhs vars' eq]
-                  end;
-                val head = print_defhead tyvars vars2 ((str o deresolve) name) vs params tys1 [] ty2;
-              in if simple then
-                concat [head, print_rhs vars2 (hd eqs)]
-              else
-                Pretty.block_enclose
-                  (concat [head, print_tuple (map (str o lookup_var vars2) params),
-                    str "match", str "{"], str "}")
-                  (map print_clause eqs)
-              end)
+                val vars' = intro_vars ((fold o Code_Thingol.fold_varnames)
+                  (insert (op =)) ts []) vars1;
+              in
+                concat [str "case",
+                  print_tuple (map (print_term tyvars true some_thm vars' NOBR) ts),
+                  str "=>", print_rhs vars' eq]
+              end;
+            val head = print_defhead tyvars vars2 name vs params tys' ty';
+          in if simple then
+            concat [head, print_rhs vars2 (hd eqs)]
+          else
+            Pretty.block_enclose
+              (concat [head, print_tuple (map (str o lookup_var vars2) params),
+                str "match", str "{"], str "}")
+              (map print_clause eqs)
+          end;
+    val print_method = (str o Library.enclose "`" "+`" o deresolve_base);
+    fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
+          print_def name (vs, ty) (filter (snd o snd) raw_eqs)
       | print_stmt (name, Code_Thingol.Datatype (_, (vs, cos))) =
           let
-            val tyvars = intro_vars (map fst vs) reserved;
+            val tyvars = intro_tyvars vs reserved;
             fun print_co ((co, _), []) =
                   concat [str "final", str "case", str "object", (str o deresolve_base) co,
-                    str "extends", applify "[" "]" NOBR ((str o deresolve_base) name)
+                    str "extends", applify "[" "]" I NOBR ((str o deresolve_base) name)
                       (replicate (length vs) (str "Nothing"))]
               | print_co ((co, vs_args), tys) =
-                  let
-                    val fields = Name.names (snd reserved) "a" tys;
-                    val vars = intro_vars (map fst fields) reserved;
-                    fun add_typargs1 p = applify "[" "]" NOBR p
-                      (map (str o lookup_tyvar tyvars o fst) vs); (*FIXME*)
-                    fun add_typargs2 p = applify "[" "]" NOBR p
-                      (map (str o lookup_tyvar tyvars) vs_args); (*FIXME*)
-                  in
-                    concat [
-                      applify "(" ")" NOBR
-                        (add_typargs2 ((concat o map str)
-                          ["final", "case", "class", deresolve_base co]))
-                        (map (uncurry (print_typed tyvars) o apfst str) fields),
-                      str "extends",
-                      add_typargs1 ((str o deresolve_base) name)
-                    ]
-                  end
+                  concat [applify "(" ")"
+                    (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg)) NOBR
+                    (applify "[" "]" (str o lookup_tyvar tyvars) NOBR ((concat o map str)
+                      ["final", "case", "class", deresolve_base co]) vs_args)
+                    (Name.names (snd reserved) "a" tys),
+                    str "extends",
+                    applify "[" "]" (str o lookup_tyvar tyvars o fst) NOBR
+                      ((str o deresolve_base) name) vs
+                  ];
           in
-            Pretty.chunks (
-              applify "[" "]" NOBR ((concat o map str)
-                  ["sealed", "class", deresolve_base name])
-                (map (str o prefix "+" o lookup_tyvar tyvars o fst) vs)
-              :: map print_co cos
-            )
+            Pretty.chunks (applify "[" "]" (str o prefix "+" o lookup_tyvar tyvars o fst)
+              NOBR ((concat o map str) ["sealed", "class", deresolve_base name]) vs
+                :: map print_co cos)
           end
       | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
           let
-            val tyvars = intro_vars [v] reserved;
-            val vs = [(v, [name])];
-            fun add_typarg p = applify "[" "]" NOBR p [(str o lookup_tyvar tyvars) v];
+            val tyvars = intro_tyvars [(v, [name])] reserved;
+            fun add_typarg s = Pretty.block
+              [str s, str "[", (str o lookup_tyvar tyvars) v, str "]"];
             fun print_super_classes [] = NONE
               | print_super_classes classes = SOME (concat (str "extends"
-                  :: separate (str "with")
-                    (map (add_typarg o str o deresolve o fst) classes)));
-            fun print_tupled_typ ([], ty) =
-                  print_typ tyvars NOBR ty
-              | print_tupled_typ ([ty1], ty2) =
-                  concat [print_typ tyvars BR ty1, str "=>", print_typ tyvars NOBR ty2]
-              | print_tupled_typ (tys, ty) =
-                  concat [enum "," "(" ")" (map (print_typ tyvars NOBR) tys),
-                    str "=>", print_typ tyvars NOBR ty];
+                  :: separate (str "with") (map (add_typarg o deresolve o fst) classes)));
             fun print_classparam_val (classparam, ty) =
-              concat [str "val", (str o Library.enclose "`" "+`:" o deresolve_base)
-                  classparam,
-                (print_tupled_typ o Code_Thingol.unfold_fun) ty]
-            fun implicit_arguments tyvars vs vars = (*FIXME simplifiy*)
-              let
-                val implicit_typ_ps = maps (fn (v, sort) => map (fn class => Pretty.block
-                  [(str o deresolve) class, str "[",
-                    (str o lookup_tyvar tyvars) v, str "]"]) sort) vs;
-                val implicit_names = Name.variant_list [] (maps (fn (v, sort) =>
-                  map (fn class => lookup_tyvar tyvars v ^ "_" ^
-                    (Long_Name.base_name o deresolve) class) sort) vs);
-                val vars' = intro_vars implicit_names vars;
-                val implicit_ps = map2 (fn v => fn p => concat [str (v ^ ":"), p])
-                  implicit_names implicit_typ_ps;
-              in ((implicit_names, implicit_ps), vars') end;
+              concat [str "val", constraint (print_method classparam)
+                ((print_tupled_typ tyvars o Code_Thingol.unfold_fun) ty)];
             fun print_classparam_def (classparam, ty) =
               let
                 val (tys, ty) = Code_Thingol.unfold_fun ty;
-                val params = Name.invents (snd reserved) "a" (length tys);
-                val vars = intro_vars params reserved;
-                val (([implicit], [p_implicit]), vars') = implicit_arguments tyvars vs vars;
-                val head = print_defhead tyvars vars' ((str o deresolve) classparam)
-                  ((map o apsnd) (K []) vs) params tys [p_implicit] ty;
+                val [implicit_name] = Name.invents (snd reserved) (lookup_tyvar tyvars v) 1;
+                val proto_vars = intro_vars [implicit_name] reserved;
+                val auxs = Name.invents (snd proto_vars) "a" (length tys);
+                val vars = intro_vars auxs proto_vars;
               in
-                concat [head, applify "(" ")" NOBR
-                  (Pretty.block [str implicit, str ".",
-                    (str o Library.enclose "`" "+`" o deresolve_base) classparam])
-                  (map (str o lookup_var vars') params)]
+                concat [str "def", constraint (Pretty.block [applify "(" ")"
+                  (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
+                  (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve classparam))
+                  (auxs ~~ tys), str "(implicit ", str implicit_name, str ": ",
+                  add_typarg (deresolve name), str ")"]) (print_typ tyvars NOBR ty), str "=",
+                  applify "(" ")" (str o lookup_var vars) NOBR
+                  (Pretty.block [str implicit_name, str ".", print_method classparam]) auxs]
               end;
           in
             Pretty.chunks (
               (Pretty.block_enclose
-                (concat ([str "trait", add_typarg ((str o deresolve_base) name)]
+                (concat ([str "trait", (add_typarg o deresolve_base) name]
                   @ the_list (print_super_classes super_classes) @ [str "{"]), str "}")
                 (map print_classparam_val classparams))
               :: map print_classparam_def classparams
@@ -276,35 +251,27 @@
       | print_stmt (name, Code_Thingol.Classinst ((class, (tyco, vs)),
             (super_instances, (classparam_instances, further_classparam_instances)))) =
           let
-            val tyvars = intro_vars (map fst vs) reserved;
-            val classtyp = (class, (tyco, map fst vs));
-            fun print_classtyp' (class, (tyco, vs)) = (*FIXME already exists?*)
-              applify "[" "]" NOBR(*? FIXME*) ((str o deresolve) class)
-                [print_typ tyvars NOBR (tyco `%% map ITyVar vs)]; (*FIXME a mess...*)
-            fun print_typed' tyvars p classtyp = (*FIXME unify with existing print_typed*)
-              Pretty.block [p, str ":", Pretty.brk 1, print_classtyp' classtyp];
-            fun print_defhead' tyvars vars p vs params tys classtyp = (*FIXME unify with existing def_head*)
-              Pretty.block [str "def ", print_typed' tyvars
-                (applify "(" ")" NOBR
-                  (applify "[" "]" NOBR p (map (fn (v, sort) =>
-                      (str o implode) (lookup_tyvar tyvars v :: map (prefix ": " o deresolve) sort)) vs))
-                    (map2 (fn param => fn ty => print_typed tyvars ((str o lookup_var vars) param) ty)
-                      params tys)) classtyp, str " ="];
+            val tyvars = intro_tyvars vs reserved;
+            val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
             fun print_classparam_instance ((classparam, const as (_, (_, tys))), (thm, _)) =
               let
-                val auxs = Name.invents (snd reserved) "a" (length tys);
+                val aux_tys = Name.names (snd reserved) "a" tys;
+                val auxs = map fst aux_tys;
                 val vars = intro_vars auxs reserved;
-                val args = if null auxs then [] else
-                  [concat [enum "," "(" ")" (map2 (fn aux => fn ty => print_typed tyvars ((str o lookup_var vars) aux) ty)
-                    auxs tys), str "=>"]];
+                val aux_abstr = if null auxs then [] else [enum "," "(" ")"
+                  (map (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
+                  (print_typ tyvars NOBR ty)) aux_tys), str "=>"];
               in 
-                concat ([str "val", (str o Library.enclose "`" "+`" o deresolve_base) classparam,
-                  str "="] @ args @ [print_app tyvars false (SOME thm) vars NOBR (const, map (IVar o SOME) auxs)])
+                concat ([str "val", print_method classparam, str "="]
+                  @ aux_abstr @| print_app tyvars false (SOME thm) vars NOBR
+                    (const, map (IVar o SOME) auxs))
               end;
-            val head = print_defhead' tyvars reserved ((str o deresolve) name) vs [] [] classtyp;
-            val body = [str "new", print_classtyp' classtyp,
-              Pretty.enum ";" "{ " " }" (map print_classparam_instance (classparam_instances @ further_classparam_instances))];
-          in concat (str "implicit" :: head :: body) end;
+          in
+            Pretty.block_enclose (concat [str "implicit def",
+              constraint (print_context tyvars vs name) (print_dicttyp tyvars classtyp),
+              str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}")
+                (map print_classparam_instance (classparam_instances @ further_classparam_instances))
+          end;
   in print_stmt end;
 
 fun scala_program_of_program labelled_name module_name reserved raw_module_alias program =
@@ -368,25 +335,24 @@
     val (deresolver, (the_module_name, sca_program)) = scala_program_of_program labelled_name
       module_name reserved raw_module_alias program;
     val reserved = make_vars reserved;
+    fun lookup_constr tyco constr = case Graph.get_node program tyco
+     of Code_Thingol.Datatype (_, (_, constrs)) =>
+          the (AList.lookup (op = o apsnd fst) constrs constr);
+    fun classparams_of_class class = case Graph.get_node program class
+     of Code_Thingol.Class (_, (_, (_, classparams))) => classparams;
     fun args_num c = case Graph.get_node program c
      of Code_Thingol.Fun (_, (((_, ty), []), _)) =>
           (length o fst o Code_Thingol.unfold_fun) ty
       | Code_Thingol.Fun (_, ((_, ((ts, _), _) :: _), _)) => length ts
-      | Code_Thingol.Datatypecons (_, tyco) =>
-          let val Code_Thingol.Datatype (_, (_, constrs)) = Graph.get_node program tyco
-          in (length o the o AList.lookup (eq_fst op =) constrs) (c, []) end (*FIXME simplify lookup*)
+      | Code_Thingol.Datatypecons (_, tyco) => length (lookup_constr tyco c)
       | Code_Thingol.Classparam (_, class) =>
-          let
-            val Code_Thingol.Class (_, (_, (_, classparams))) =
-              Graph.get_node program class
-          in (length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =) classparams) c end;
-    fun is_singleton c = case Graph.get_node program c
-     of Code_Thingol.Datatypecons (_, tyco) =>
-          let val Code_Thingol.Datatype (_, (_, constrs)) = Graph.get_node program tyco
-          in (null o the o AList.lookup (eq_fst op =) constrs) (c, []) end (*FIXME simplify lookup*)
+          (length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =)
+            (classparams_of_class class)) c;
+    fun is_singleton_constr c = case Graph.get_node program c
+     of Code_Thingol.Datatypecons (_, tyco) => null (lookup_constr tyco c)
       | _ => false;
     val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
-      reserved args_num is_singleton deresolver;
+      reserved args_num is_singleton_constr deresolver;
     fun print_module name content =
       (name, Pretty.chunks [
         str ("object " ^ name ^ " {"),
@@ -468,7 +434,7 @@
       "true", "type", "val", "var", "while", "with", "yield"
     ]
   #> fold (Code_Target.add_reserved target) [
-      "error", "apply", "List", "Nil", "BigInt"
+      "apply", "error", "BigInt", "Nil", "List"
     ];
 
 end; (*struct*)
--- a/src/Tools/Code/code_thingol.ML	Wed Jun 30 18:03:34 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML	Wed Jun 30 18:19:53 2010 +0200
@@ -40,6 +40,7 @@
   val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list
   val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a
   val unfold_fun: itype -> itype list * itype
+  val unfold_fun_n: int -> itype -> itype list * itype
   val unfold_app: iterm -> iterm * iterm list
   val unfold_abs: iterm -> (vname option * itype) list * iterm
   val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option
@@ -396,6 +397,13 @@
   (fn tyco `%% [ty1, ty2] => if tyco = fun_tyco then SOME (ty1, ty2) else NONE
     | _ => NONE);
 
+fun unfold_fun_n n ty =
+  let
+    val (tys1, ty1) = unfold_fun ty;
+    val (tys3, tys2) = chop n tys1;
+    val ty3 = Library.foldr (fn (ty1, ty2) => fun_tyco `%% [ty1, ty2]) (tys2, ty1);
+  in (tys3, ty3) end;
+
 end; (* local *)