explicit check for pattern discipline before code translation
authorhaftmann
Wed Oct 29 11:33:40 2008 +0100 (2008-10-29)
changeset 28708a1a436f09ec6
parent 28707 548703affff5
child 28709 6a5d214aaa82
explicit check for pattern discipline before code translation
src/HOL/Library/Code_Index.thy
src/HOL/Library/Multiset.thy
src/HOL/List.thy
src/HOL/Tools/numeral.ML
src/Pure/Isar/code.ML
src/Pure/Isar/code_unit.ML
src/Tools/code/code_haskell.ML
src/Tools/code/code_ml.ML
src/Tools/code/code_printer.ML
src/Tools/code/code_thingol.ML
     1.1 --- a/src/HOL/Library/Code_Index.thy	Tue Oct 28 17:53:46 2008 +0100
     1.2 +++ b/src/HOL/Library/Code_Index.thy	Wed Oct 29 11:33:40 2008 +0100
     1.3 @@ -27,6 +27,9 @@
     1.4    by (rule index_of_nat_inverse) 
     1.5      (unfold index_def, rule UNIV_I)
     1.6  
     1.7 +lemma [measure_function]:
     1.8 +  "is_measure nat_of_index" by (rule is_measure_trivial)
     1.9 +
    1.10  lemma index:
    1.11    "(\<And>n\<Colon>index. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (index_of_nat n))"
    1.12  proof
    1.13 @@ -143,70 +146,73 @@
    1.14  instantiation index :: "{minus, ordered_semidom, Divides.div, linorder}"
    1.15  begin
    1.16  
    1.17 -lemma zero_index_code [code inline, code]:
    1.18 -  "(0\<Colon>index) = Numeral0"
    1.19 -  by (simp add: number_of_index_def Pls_def)
    1.20 -lemma [code post]: "Numeral0 = (0\<Colon>index)"
    1.21 -  using zero_index_code ..
    1.22 -
    1.23  definition [simp, code del]:
    1.24    "(1\<Colon>index) = index_of_nat 1"
    1.25  
    1.26 -lemma one_index_code [code inline, code]:
    1.27 -  "(1\<Colon>index) = Numeral1"
    1.28 -  by (simp add: number_of_index_def Pls_def Bit1_def)
    1.29 -lemma [code post]: "Numeral1 = (1\<Colon>index)"
    1.30 -  using one_index_code ..
    1.31 -
    1.32  definition [simp, code del]:
    1.33    "n + m = index_of_nat (nat_of_index n + nat_of_index m)"
    1.34  
    1.35 -lemma plus_index_code [code]:
    1.36 -  "index_of_nat n + index_of_nat m = index_of_nat (n + m)"
    1.37 -  by simp
    1.38 -
    1.39  definition [simp, code del]:
    1.40    "n - m = index_of_nat (nat_of_index n - nat_of_index m)"
    1.41  
    1.42  definition [simp, code del]:
    1.43    "n * m = index_of_nat (nat_of_index n * nat_of_index m)"
    1.44  
    1.45 -lemma times_index_code [code]:
    1.46 -  "index_of_nat n * index_of_nat m = index_of_nat (n * m)"
    1.47 -  by simp
    1.48 -
    1.49  definition [simp, code del]:
    1.50    "n div m = index_of_nat (nat_of_index n div nat_of_index m)"
    1.51  
    1.52  definition [simp, code del]:
    1.53    "n mod m = index_of_nat (nat_of_index n mod nat_of_index m)"
    1.54  
    1.55 -lemma div_index_code [code]:
    1.56 -  "index_of_nat n div index_of_nat m = index_of_nat (n div m)"
    1.57 -  by simp
    1.58 -
    1.59 -lemma mod_index_code [code]:
    1.60 -  "index_of_nat n mod index_of_nat m = index_of_nat (n mod m)"
    1.61 -  by simp
    1.62 -
    1.63  definition [simp, code del]:
    1.64    "n \<le> m \<longleftrightarrow> nat_of_index n \<le> nat_of_index m"
    1.65  
    1.66  definition [simp, code del]:
    1.67    "n < m \<longleftrightarrow> nat_of_index n < nat_of_index m"
    1.68  
    1.69 -lemma less_eq_index_code [code]:
    1.70 +instance by default (auto simp add: left_distrib index)
    1.71 +
    1.72 +end
    1.73 +
    1.74 +lemma zero_index_code [code inline, code]:
    1.75 +  "(0\<Colon>index) = Numeral0"
    1.76 +  by (simp add: number_of_index_def Pls_def)
    1.77 +lemma [code post]: "Numeral0 = (0\<Colon>index)"
    1.78 +  using zero_index_code ..
    1.79 +
    1.80 +lemma one_index_code [code inline, code]:
    1.81 +  "(1\<Colon>index) = Numeral1"
    1.82 +  by (simp add: number_of_index_def Pls_def Bit1_def)
    1.83 +lemma [code post]: "Numeral1 = (1\<Colon>index)"
    1.84 +  using one_index_code ..
    1.85 +
    1.86 +lemma plus_index_code [code nbe]:
    1.87 +  "index_of_nat n + index_of_nat m = index_of_nat (n + m)"
    1.88 +  by simp
    1.89 +
    1.90 +definition subtract_index :: "index \<Rightarrow> index \<Rightarrow> index" where
    1.91 +  [simp, code del]: "subtract_index = op -"
    1.92 +
    1.93 +lemma subtract_index_code [code nbe]:
    1.94 +  "subtract_index (index_of_nat n) (index_of_nat m) = index_of_nat (n - m)"
    1.95 +  by simp
    1.96 +
    1.97 +lemma minus_index_code [code]:
    1.98 +  "n - m = subtract_index n m"
    1.99 +  by simp
   1.100 +
   1.101 +lemma times_index_code [code nbe]:
   1.102 +  "index_of_nat n * index_of_nat m = index_of_nat (n * m)"
   1.103 +  by simp
   1.104 +
   1.105 +lemma less_eq_index_code [code nbe]:
   1.106    "index_of_nat n \<le> index_of_nat m \<longleftrightarrow> n \<le> m"
   1.107    by simp
   1.108  
   1.109 -lemma less_index_code [code]:
   1.110 +lemma less_index_code [code nbe]:
   1.111    "index_of_nat n < index_of_nat m \<longleftrightarrow> n < m"
   1.112    by simp
   1.113  
   1.114 -instance by default (auto simp add: left_distrib index)
   1.115 -
   1.116 -end
   1.117 -
   1.118  lemma Suc_index_minus_one: "Suc_index n - 1 = n" by simp
   1.119  
   1.120  lemma index_of_nat_code [code]:
   1.121 @@ -222,9 +228,7 @@
   1.122  lemma index_not_eq_zero: "i \<noteq> index_of_nat 0 \<longleftrightarrow> i \<ge> 1"
   1.123    by (cases i) auto
   1.124  
   1.125 -definition
   1.126 -  nat_of_index_aux :: "index \<Rightarrow> nat \<Rightarrow> nat"
   1.127 -where
   1.128 +definition nat_of_index_aux :: "index \<Rightarrow> nat \<Rightarrow> nat" where
   1.129    "nat_of_index_aux i n = nat_of_index i + n"
   1.130  
   1.131  lemma nat_of_index_aux_code [code]:
   1.132 @@ -235,39 +239,7 @@
   1.133    "nat_of_index i = nat_of_index_aux i 0"
   1.134    by (simp add: nat_of_index_aux_def)
   1.135  
   1.136 -
   1.137 -text {* Measure function (for termination proofs) *}
   1.138 -
   1.139 -lemma [measure_function]:
   1.140 -  "is_measure nat_of_index" by (rule is_measure_trivial)
   1.141 -
   1.142 -subsection {* ML interface *}
   1.143 -
   1.144 -ML {*
   1.145 -structure Index =
   1.146 -struct
   1.147 -
   1.148 -fun mk k = HOLogic.mk_number @{typ index} k;
   1.149 -
   1.150 -end;
   1.151 -*}
   1.152 -
   1.153 -
   1.154 -subsection {* Specialized @{term "op - \<Colon> index \<Rightarrow> index \<Rightarrow> index"},
   1.155 -  @{term "op div \<Colon> index \<Rightarrow> index \<Rightarrow> index"} and @{term "op mod \<Colon> index \<Rightarrow> index \<Rightarrow> index"}
   1.156 -  operations *}
   1.157 -
   1.158 -definition
   1.159 -  minus_index_aux :: "index \<Rightarrow> index \<Rightarrow> index"
   1.160 -where
   1.161 -  [code del]: "minus_index_aux = op -"
   1.162 -
   1.163 -lemma [code]: "op - = minus_index_aux"
   1.164 -  using minus_index_aux_def ..
   1.165 -
   1.166 -definition
   1.167 -  div_mod_index ::  "index \<Rightarrow> index \<Rightarrow> index \<times> index"
   1.168 -where
   1.169 +definition div_mod_index ::  "index \<Rightarrow> index \<Rightarrow> index \<times> index" where
   1.170    [code del]: "div_mod_index n m = (n div m, n mod m)"
   1.171  
   1.172  lemma [code]:
   1.173 @@ -283,6 +255,18 @@
   1.174    unfolding div_mod_index_def by simp
   1.175  
   1.176  
   1.177 +subsection {* ML interface *}
   1.178 +
   1.179 +ML {*
   1.180 +structure Index =
   1.181 +struct
   1.182 +
   1.183 +fun mk k = HOLogic.mk_number @{typ index} k;
   1.184 +
   1.185 +end;
   1.186 +*}
   1.187 +
   1.188 +
   1.189  subsection {* Code generator setup *}
   1.190  
   1.191  text {* Implementation of indices by bounded integers *}
   1.192 @@ -308,7 +292,7 @@
   1.193    (OCaml "Pervasives.( + )")
   1.194    (Haskell infixl 6 "+")
   1.195  
   1.196 -code_const "minus_index_aux \<Colon> index \<Rightarrow> index \<Rightarrow> index"
   1.197 +code_const "subtract_index \<Colon> index \<Rightarrow> index \<Rightarrow> index"
   1.198    (SML "Int.max/ (_/ -/ _,/ 0 : int)")
   1.199    (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ")
   1.200    (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
     2.1 --- a/src/HOL/Library/Multiset.thy	Tue Oct 28 17:53:46 2008 +0100
     2.2 +++ b/src/HOL/Library/Multiset.thy	Wed Oct 29 11:33:40 2008 +0100
     2.3 @@ -20,27 +20,19 @@
     2.4      Abs_multiset_inverse Rep_multiset_inverse Rep_multiset
     2.5    and [simp] = Rep_multiset_inject [symmetric]
     2.6  
     2.7 -definition
     2.8 -  Mempty :: "'a multiset"  ("{#}") where
     2.9 -  "{#} = Abs_multiset (\<lambda>a. 0)"
    2.10 +definition Mempty :: "'a multiset"  ("{#}") where
    2.11 +  [code del]: "{#} = Abs_multiset (\<lambda>a. 0)"
    2.12  
    2.13 -definition
    2.14 -  single :: "'a => 'a multiset" where
    2.15 -  "single a = Abs_multiset (\<lambda>b. if b = a then 1 else 0)"
    2.16 +definition single :: "'a => 'a multiset" where
    2.17 +  [code del]: "single a = Abs_multiset (\<lambda>b. if b = a then 1 else 0)"
    2.18  
    2.19 -declare
    2.20 -  Mempty_def[code del] single_def[code del]
    2.21 -
    2.22 -definition
    2.23 -  count :: "'a multiset => 'a => nat" where
    2.24 +definition count :: "'a multiset => 'a => nat" where
    2.25    "count = Rep_multiset"
    2.26  
    2.27 -definition
    2.28 -  MCollect :: "'a multiset => ('a => bool) => 'a multiset" where
    2.29 +definition MCollect :: "'a multiset => ('a => bool) => 'a multiset" where
    2.30    "MCollect M P = Abs_multiset (\<lambda>x. if P x then Rep_multiset M x else 0)"
    2.31  
    2.32 -abbreviation
    2.33 -  Melem :: "'a => 'a multiset => bool"  ("(_/ :# _)" [50, 51] 50) where
    2.34 +abbreviation Melem :: "'a => 'a multiset => bool"  ("(_/ :# _)" [50, 51] 50) where
    2.35    "a :# M == 0 < count M a"
    2.36  
    2.37  notation (xsymbols)
    2.38 @@ -51,25 +43,23 @@
    2.39  translations
    2.40    "{#x :# M. P#}" == "CONST MCollect M (\<lambda>x. P)"
    2.41  
    2.42 -definition
    2.43 -  set_of :: "'a multiset => 'a set" where
    2.44 +definition set_of :: "'a multiset => 'a set" where
    2.45    "set_of M = {x. x :# M}"
    2.46  
    2.47  instantiation multiset :: (type) "{plus, minus, zero, size}" 
    2.48  begin
    2.49  
    2.50 -definition
    2.51 -  union_def[code del]:
    2.52 +definition union_def [code del]:
    2.53    "M + N = Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
    2.54  
    2.55 -definition
    2.56 -  diff_def: "M - N = Abs_multiset (\<lambda>a. Rep_multiset M a - Rep_multiset N a)"
    2.57 +definition diff_def [code del]:
    2.58 +  "M - N = Abs_multiset (\<lambda>a. Rep_multiset M a - Rep_multiset N a)"
    2.59  
    2.60 -definition
    2.61 -  Zero_multiset_def [simp]: "0 = {#}"
    2.62 +definition Zero_multiset_def [simp]:
    2.63 +  "0 = {#}"
    2.64  
    2.65 -definition
    2.66 -  size_def[code del]: "size M = setsum (count M) (set_of M)"
    2.67 +definition size_def:
    2.68 +  "size M = setsum (count M) (set_of M)"
    2.69  
    2.70  instance ..
    2.71  
    2.72 @@ -207,10 +197,10 @@
    2.73  
    2.74  subsubsection {* Size *}
    2.75  
    2.76 -lemma size_empty [simp,code]: "size {#} = 0"
    2.77 +lemma size_empty [simp]: "size {#} = 0"
    2.78  by (simp add: size_def)
    2.79  
    2.80 -lemma size_single [simp,code]: "size {#b#} = 1"
    2.81 +lemma size_single [simp]: "size {#b#} = 1"
    2.82  by (simp add: size_def)
    2.83  
    2.84  lemma finite_set_of [iff]: "finite (set_of M)"
    2.85 @@ -223,7 +213,7 @@
    2.86  apply (simp add: Int_insert_left set_of_def)
    2.87  done
    2.88  
    2.89 -lemma size_union[simp,code]: "size (M + N::'a multiset) = size M + size N"
    2.90 +lemma size_union [simp]: "size (M + N::'a multiset) = size M + size N"
    2.91  apply (unfold size_def)
    2.92  apply (subgoal_tac "count (M + N) = (\<lambda>a. count M a + count N a)")
    2.93   prefer 2
    2.94 @@ -376,16 +366,16 @@
    2.95  
    2.96  subsubsection {* Comprehension (filter) *}
    2.97  
    2.98 -lemma MCollect_empty[simp, code]: "MCollect {#} P = {#}"
    2.99 +lemma MCollect_empty [simp]: "MCollect {#} P = {#}"
   2.100  by (simp add: MCollect_def Mempty_def Abs_multiset_inject
   2.101      in_multiset expand_fun_eq)
   2.102  
   2.103 -lemma MCollect_single[simp, code]:
   2.104 +lemma MCollect_single [simp]:
   2.105    "MCollect {#x#} P = (if P x then {#x#} else {#})"
   2.106  by (simp add: MCollect_def Mempty_def single_def Abs_multiset_inject
   2.107      in_multiset expand_fun_eq)
   2.108  
   2.109 -lemma MCollect_union[simp, code]:
   2.110 +lemma MCollect_union [simp]:
   2.111    "MCollect (M+N) f = MCollect M f + MCollect N f"
   2.112  by (simp add: MCollect_def union_def Abs_multiset_inject
   2.113      in_multiset expand_fun_eq)
   2.114 @@ -498,14 +488,11 @@
   2.115  
   2.116  subsubsection {* Well-foundedness *}
   2.117  
   2.118 -definition
   2.119 -  mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
   2.120 -  [code del]:"mult1 r =
   2.121 -    {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
   2.122 +definition mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
   2.123 +  [code del]: "mult1 r = {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
   2.124        (\<forall>b. b :# K --> (b, a) \<in> r)}"
   2.125  
   2.126 -definition
   2.127 -  mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
   2.128 +definition mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
   2.129    "mult r = (mult1 r)\<^sup>+"
   2.130  
   2.131  lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
   2.132 @@ -715,11 +702,11 @@
   2.133  instantiation multiset :: (order) order
   2.134  begin
   2.135  
   2.136 -definition
   2.137 -  less_multiset_def [code del]: "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
   2.138 +definition less_multiset_def [code del]:
   2.139 +  "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
   2.140  
   2.141 -definition
   2.142 -  le_multiset_def [code del]: "M' <= M \<longleftrightarrow> M' = M \<or> M' < (M::'a multiset)"
   2.143 +definition le_multiset_def [code del]:
   2.144 +  "M' <= M \<longleftrightarrow> M' = M \<or> M' < (M::'a multiset)"
   2.145  
   2.146  lemma trans_base_order: "trans {(x', x). x' < (x::'a::order)}"
   2.147  unfolding trans_def by (blast intro: order_less_trans)
   2.148 @@ -981,13 +968,11 @@
   2.149  
   2.150  subsection {* Pointwise ordering induced by count *}
   2.151  
   2.152 -definition
   2.153 -  mset_le :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<le>#" 50) where
   2.154 -  [code del]: "(A \<le># B) = (\<forall>a. count A a \<le> count B a)"
   2.155 +definition mset_le :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<le>#" 50) where
   2.156 +  [code del]: "A \<le># B \<longleftrightarrow> (\<forall>a. count A a \<le> count B a)"
   2.157  
   2.158 -definition
   2.159 -  mset_less :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "<#" 50) where
   2.160 -  [code del]: "(A <# B) = (A \<le># B \<and> A \<noteq> B)"
   2.161 +definition mset_less :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "<#" 50) where
   2.162 +  [code del]: "A <# B \<longleftrightarrow> A \<le># B \<and> A \<noteq> B"
   2.163  
   2.164  notation mset_le  (infix "\<subseteq>#" 50)
   2.165  notation mset_less  (infix "\<subset>#" 50)
   2.166 @@ -1448,22 +1433,23 @@
   2.167  
   2.168  subsection {* Image *}
   2.169  
   2.170 -definition [code del]: "image_mset f == fold_mset (op + o single o f) {#}"
   2.171 +definition [code del]:
   2.172 + "image_mset f = fold_mset (op + o single o f) {#}"
   2.173  
   2.174  interpretation image_left_comm: left_commutative ["op + o single o f"]
   2.175  by (unfold_locales) (simp add:union_ac)
   2.176  
   2.177 -lemma image_mset_empty [simp, code]: "image_mset f {#} = {#}"
   2.178 +lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
   2.179  by (simp add: image_mset_def)
   2.180  
   2.181 -lemma image_mset_single [simp, code]: "image_mset f {#x#} = {#f x#}"
   2.182 +lemma image_mset_single [simp]: "image_mset f {#x#} = {#f x#}"
   2.183  by (simp add: image_mset_def)
   2.184  
   2.185  lemma image_mset_insert:
   2.186    "image_mset f (M + {#a#}) = image_mset f M + {#f a#}"
   2.187  by (simp add: image_mset_def add_ac)
   2.188  
   2.189 -lemma image_mset_union[simp, code]:
   2.190 +lemma image_mset_union [simp]:
   2.191    "image_mset f (M+N) = image_mset f M + image_mset f N"
   2.192  apply (induct N)
   2.193   apply simp
   2.194 @@ -1476,7 +1462,6 @@
   2.195  lemma image_mset_is_empty_iff [simp]: "image_mset f M = {#} \<longleftrightarrow> M = {#}"
   2.196  by (cases M) auto
   2.197  
   2.198 -
   2.199  syntax
   2.200    comprehension1_mset :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
   2.201        ("({#_/. _ :# _#})")
     3.1 --- a/src/HOL/List.thy	Tue Oct 28 17:53:46 2008 +0100
     3.2 +++ b/src/HOL/List.thy	Wed Oct 29 11:33:40 2008 +0100
     3.3 @@ -3578,7 +3578,7 @@
     3.4  fun pretty_list literals =
     3.5    let
     3.6      val mk_list = Code_Printer.literal_list literals;
     3.7 -    fun pretty pr naming thm pat vars fxy [(t1, _), (t2, _)] =
     3.8 +    fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] =
     3.9        case Option.map (cons t1) (implode_list (list_names naming) t2)
    3.10         of SOME ts => mk_list (map (pr vars Code_Printer.NOBR) ts)
    3.11          | NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
    3.12 @@ -3589,7 +3589,7 @@
    3.13      val mk_list = Code_Printer.literal_list literals;
    3.14      val mk_char = Code_Printer.literal_char literals;
    3.15      val mk_string = Code_Printer.literal_string literals;
    3.16 -    fun pretty pr naming thm pat vars fxy [(t1, _), (t2, _)] =
    3.17 +    fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] =
    3.18        case Option.map (cons t1) (implode_list (list_names naming) t2)
    3.19         of SOME ts => (case implode_string (char_name naming, nibble_names naming) mk_char mk_string ts
    3.20             of SOME p => p
    3.21 @@ -3600,7 +3600,7 @@
    3.22  fun pretty_char literals =
    3.23    let
    3.24      val mk_char = Code_Printer.literal_char literals;
    3.25 -    fun pretty _ naming thm _ _ _ [(t1, _), (t2, _)] =
    3.26 +    fun pretty _ naming thm _ _ [(t1, _), (t2, _)] =
    3.27        case decode_char (nibble_names naming) (t1, t2)
    3.28         of SOME c => (Code_Printer.str o mk_char) c
    3.29          | NONE => Code_Printer.nerror thm "Illegal character expression";
    3.30 @@ -3610,7 +3610,7 @@
    3.31    let
    3.32      val mk_char = Code_Printer.literal_char literals;
    3.33      val mk_string = Code_Printer.literal_string literals;
    3.34 -    fun pretty _ naming thm _ _ _ [(t, _)] =
    3.35 +    fun pretty _ naming thm _ _ [(t, _)] =
    3.36        case implode_list (list_names naming) t
    3.37         of SOME ts => (case implode_string (char_name naming, nibble_names naming) mk_char mk_string ts
    3.38             of SOME p => p
     4.1 --- a/src/HOL/Tools/numeral.ML	Tue Oct 28 17:53:46 2008 +0100
     4.2 +++ b/src/HOL/Tools/numeral.ML	Wed Oct 29 11:33:40 2008 +0100
     4.3 @@ -79,7 +79,7 @@
     4.4                in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
     4.5            | dest_num _ = Code_Printer.nerror thm "Illegal numeral expression: illegal term";
     4.6        in dest_num end;
     4.7 -    fun pretty _ naming thm _ _ _ [(t, _)] =
     4.8 +    fun pretty _ naming thm _ _ [(t, _)] =
     4.9        (Code_Printer.str o pr_numeral unbounded o the_default 0 o dest_numeral naming thm) t;
    4.10    in
    4.11      thy
     5.1 --- a/src/Pure/Isar/code.ML	Tue Oct 28 17:53:46 2008 +0100
     5.2 +++ b/src/Pure/Isar/code.ML	Wed Oct 29 11:33:40 2008 +0100
     5.3 @@ -462,13 +462,6 @@
     5.4            cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
     5.5        in map (Thm.instantiate (instT, [])) thms' end;
     5.6  
     5.7 -fun certify_const thy c eqns =
     5.8 -  let
     5.9 -    fun cert (eqn as (thm, _)) = if c = Code_Unit.const_eqn thm
    5.10 -      then eqn else error ("Wrong head of defining equation,\nexpected constant "
    5.11 -        ^ Code_Unit.string_of_const thy c ^ "\n" ^ Display.string_of_thm thm)
    5.12 -  in map cert eqns end;
    5.13 -
    5.14  fun check_linear (eqn as (thm, linear)) =
    5.15    if linear then eqn else Code_Unit.bad_thm
    5.16      ("Duplicate variables on left hand side of defining equation:\n"
    5.17 @@ -542,6 +535,16 @@
    5.18          in SOME (Logic.varifyT ty) end
    5.19      | NONE => NONE;
    5.20  
    5.21 +fun recheck_eqn thy = Code_Unit.error_thm
    5.22 +  (Code_Unit.assert_linear (is_some o get_datatype_of_constr thy) o apfst (Code_Unit.assert_eqn thy));
    5.23 +
    5.24 +fun recheck_eqns_const thy c eqns =
    5.25 +  let
    5.26 +    fun cert (eqn as (thm, _)) = if c = Code_Unit.const_eqn thm
    5.27 +      then eqn else error ("Wrong head of defining equation,\nexpected constant "
    5.28 +        ^ Code_Unit.string_of_const thy c ^ "\n" ^ Display.string_of_thm thm)
    5.29 +  in map (cert o recheck_eqn thy) eqns end;
    5.30 +
    5.31  fun change_eqns delete c f = (map_exec_purge (SOME [c]) o map_eqns
    5.32    o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, Lazy.value [])), [])))
    5.33      o apfst) (fn (_, eqns) => (true, f eqns));
    5.34 @@ -568,8 +571,7 @@
    5.35  
    5.36  fun add_eqnl (c, lthms) thy =
    5.37    let
    5.38 -    val lthms' = certificate thy
    5.39 -      (fn thy => map (Code_Unit.assert_linear) o certify_const thy c) lthms;
    5.40 +    val lthms' = certificate thy (fn thy => recheck_eqns_const thy c) lthms;
    5.41    in change_eqns false c (add_lthms lthms') thy end;
    5.42  
    5.43  val add_default_eqn_attribute = Thm.declaration_attribute
    5.44 @@ -660,8 +662,7 @@
    5.45    | apply_functrans thy c functrans eqns = eqns
    5.46        |> perhaps (perhaps_loop (perhaps_apply functrans))
    5.47        |> (map o apfst) (AxClass.unoverload thy)
    5.48 -      |> (map o Code_Unit.error_thm) (Code_Unit.assert_linear o apfst (Code_Unit.assert_eqn thy))
    5.49 -      |> certify_const thy c
    5.50 +      |> recheck_eqns_const thy c
    5.51        |> (map o apfst) (AxClass.overload thy);
    5.52  
    5.53  fun rhs_conv conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);
    5.54 @@ -682,7 +683,7 @@
    5.55      |> apply_functrans thy c functrans
    5.56      |> (map o apfst) (Code_Unit.rewrite_eqn pre)
    5.57      |> (map o apfst) (AxClass.unoverload thy)
    5.58 -    |> map (Code_Unit.assert_linear o apfst (Code_Unit.assert_eqn thy))
    5.59 +    |> map (recheck_eqn thy)
    5.60      |> burrow_fst (common_typ_eqns thy)
    5.61    end;
    5.62  
     6.1 --- a/src/Pure/Isar/code_unit.ML	Tue Oct 28 17:53:46 2008 +0100
     6.2 +++ b/src/Pure/Isar/code_unit.ML	Wed Oct 29 11:33:40 2008 +0100
     6.3 @@ -38,7 +38,7 @@
     6.4    (*defining equations*)
     6.5    val assert_eqn: theory -> thm -> thm
     6.6    val mk_eqn: theory -> thm -> thm * bool
     6.7 -  val assert_linear: thm * bool -> thm * bool
     6.8 +  val assert_linear: (string -> bool) -> thm * bool -> thm * bool
     6.9    val const_eqn: thm -> string
    6.10    val const_typ_eqn: thm -> string * typ
    6.11    val head_eqn: theory -> thm -> string * ((string * sort) list * typ)
    6.12 @@ -377,8 +377,17 @@
    6.13        ((fold o fold_aterms) (fn Var (v, _) => cons v | _ => I) args []))
    6.14    in (thm, linear) end;
    6.15  
    6.16 -fun assert_linear (thm, false) = (thm, false)
    6.17 -  | assert_linear (thm, true) = if snd (add_linear thm) then (thm, true)
    6.18 +fun assert_pat is_cons thm =
    6.19 +  let
    6.20 +    val args = (snd o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm;
    6.21 +    val _ = (map o map_aterms) (fn t as Const (c, _) => if is_cons c then t
    6.22 +          else bad_thm ("Not a constructor on left hand side of equation: "
    6.23 +            ^ quote c ^ ",\n in equation\n" ^ Display.string_of_thm thm)
    6.24 +      | t => t) args;
    6.25 +  in thm end;
    6.26 +
    6.27 +fun assert_linear is_cons (thm, false) = (thm, false)
    6.28 +  | assert_linear is_cons (thm, true) = if snd (add_linear (assert_pat is_cons thm)) then (thm, true)
    6.29        else bad_thm
    6.30          ("Duplicate variables on left hand side of defining equation:\n"
    6.31            ^ Display.string_of_thm thm);
     7.1 --- a/src/Tools/code/code_haskell.ML	Tue Oct 28 17:53:46 2008 +0100
     7.2 +++ b/src/Tools/code/code_haskell.ML	Wed Oct 29 11:33:40 2008 +0100
     7.3 @@ -59,45 +59,45 @@
     7.4        Pretty.block (pr_typcontext tyvars vs @| pr_tycoexpr tyvars NOBR tycoexpr);
     7.5      fun pr_typscheme tyvars (vs, ty) =
     7.6        Pretty.block (pr_typforall tyvars vs @ pr_typcontext tyvars vs @| pr_typ tyvars NOBR ty);
     7.7 -    fun pr_term tyvars thm pat vars fxy (IConst c) =
     7.8 -          pr_app tyvars thm pat vars fxy (c, [])
     7.9 -      | pr_term tyvars thm pat vars fxy (t as (t1 `$ t2)) =
    7.10 +    fun pr_term tyvars thm vars fxy (IConst c) =
    7.11 +          pr_app tyvars thm vars fxy (c, [])
    7.12 +      | pr_term tyvars thm vars fxy (t as (t1 `$ t2)) =
    7.13            (case Code_Thingol.unfold_const_app t
    7.14 -           of SOME app => pr_app tyvars thm pat vars fxy app
    7.15 +           of SOME app => pr_app tyvars thm vars fxy app
    7.16              | _ =>
    7.17                  brackify fxy [
    7.18 -                  pr_term tyvars thm pat vars NOBR t1,
    7.19 -                  pr_term tyvars thm pat vars BR t2
    7.20 +                  pr_term tyvars thm vars NOBR t1,
    7.21 +                  pr_term tyvars thm vars BR t2
    7.22                  ])
    7.23 -      | pr_term tyvars thm pat vars fxy (IVar v) =
    7.24 +      | pr_term tyvars thm vars fxy (IVar v) =
    7.25            (str o Code_Name.lookup_var vars) v
    7.26 -      | pr_term tyvars thm pat vars fxy (t as _ `|-> _) =
    7.27 +      | pr_term tyvars thm vars fxy (t as _ `|-> _) =
    7.28            let
    7.29              val (binds, t') = Code_Thingol.unfold_abs t;
    7.30              fun pr ((v, pat), ty) = pr_bind tyvars thm BR ((SOME v, pat), ty);
    7.31              val (ps, vars') = fold_map pr binds vars;
    7.32 -          in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars thm pat vars' NOBR t') end
    7.33 -      | pr_term tyvars thm pat vars fxy (ICase (cases as (_, t0))) =
    7.34 +          in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars thm vars' NOBR t') end
    7.35 +      | pr_term tyvars thm vars fxy (ICase (cases as (_, t0))) =
    7.36            (case Code_Thingol.unfold_const_app t0
    7.37             of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
    7.38                  then pr_case tyvars thm vars fxy cases
    7.39 -                else pr_app tyvars thm pat vars fxy c_ts
    7.40 +                else pr_app tyvars thm vars fxy c_ts
    7.41              | NONE => pr_case tyvars thm vars fxy cases)
    7.42 -    and pr_app' tyvars thm pat vars ((c, (_, tys)), ts) = case contr_classparam_typs c
    7.43 -     of [] => (str o deresolve) c :: map (pr_term tyvars thm pat vars BR) ts
    7.44 +    and pr_app' tyvars thm vars ((c, (_, tys)), ts) = case contr_classparam_typs c
    7.45 +     of [] => (str o deresolve) c :: map (pr_term tyvars thm vars BR) ts
    7.46        | fingerprint => let
    7.47            val ts_fingerprint = ts ~~ curry Library.take (length ts) fingerprint;
    7.48            val needs_annotation = forall (fn (_, NONE) => true | (t, SOME _) =>
    7.49              (not o Code_Thingol.locally_monomorphic) t) ts_fingerprint;
    7.50 -          fun pr_term_anno (t, NONE) _ = pr_term tyvars thm pat vars BR t
    7.51 +          fun pr_term_anno (t, NONE) _ = pr_term tyvars thm vars BR t
    7.52              | pr_term_anno (t, SOME _) ty =
    7.53 -                brackets [pr_term tyvars thm pat vars NOBR t, str "::", pr_typ tyvars NOBR ty];
    7.54 +                brackets [pr_term tyvars thm vars NOBR t, str "::", pr_typ tyvars NOBR ty];
    7.55          in
    7.56            if needs_annotation then
    7.57              (str o deresolve) c :: map2 pr_term_anno ts_fingerprint (curry Library.take (length ts) tys)
    7.58 -          else (str o deresolve) c :: map (pr_term tyvars thm pat vars BR) ts
    7.59 +          else (str o deresolve) c :: map (pr_term tyvars thm vars BR) ts
    7.60          end
    7.61 -    and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const is_cons naming
    7.62 +    and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const naming
    7.63      and pr_bind tyvars = pr_haskell_bind (pr_term tyvars)
    7.64      and pr_case tyvars thm vars fxy (cases as ((_, [_]), _)) =
    7.65            let
    7.66 @@ -105,12 +105,12 @@
    7.67              fun pr ((pat, ty), t) vars =
    7.68                vars
    7.69                |> pr_bind tyvars thm BR ((NONE, SOME pat), ty)
    7.70 -              |>> (fn p => semicolon [p, str "=", pr_term tyvars thm false vars NOBR t])
    7.71 +              |>> (fn p => semicolon [p, str "=", pr_term tyvars thm vars NOBR t])
    7.72              val (ps, vars') = fold_map pr binds vars;
    7.73            in
    7.74              Pretty.block_enclose (
    7.75                str "let {",
    7.76 -              concat [str "}", str "in", pr_term tyvars thm false vars' NOBR t]
    7.77 +              concat [str "}", str "in", pr_term tyvars thm vars' NOBR t]
    7.78              ) ps
    7.79            end
    7.80        | pr_case tyvars thm vars fxy (((td, ty), bs as _ :: _), _) =
    7.81 @@ -118,10 +118,10 @@
    7.82              fun pr (pat, t) =
    7.83                let
    7.84                  val (p, vars') = pr_bind tyvars thm NOBR ((NONE, SOME pat), ty) vars;
    7.85 -              in semicolon [p, str "->", pr_term tyvars thm false vars' NOBR t] end;
    7.86 +              in semicolon [p, str "->", pr_term tyvars thm vars' NOBR t] end;
    7.87            in
    7.88              Pretty.block_enclose (
    7.89 -              concat [str "(case", pr_term tyvars thm false vars NOBR td, str "of", str "{"],
    7.90 +              concat [str "(case", pr_term tyvars thm vars NOBR td, str "of", str "{"],
    7.91                str "})"
    7.92              ) (map pr bs)
    7.93            end
    7.94 @@ -165,9 +165,9 @@
    7.95                in
    7.96                  semicolon (
    7.97                    (str o deresolve_base) name
    7.98 -                  :: map (pr_term tyvars thm true vars BR) ts
    7.99 +                  :: map (pr_term tyvars thm vars BR) ts
   7.100                    @ str "="
   7.101 -                  @@ pr_term tyvars thm false vars NOBR t
   7.102 +                  @@ pr_term tyvars thm vars NOBR t
   7.103                  )
   7.104                end;
   7.105            in
   7.106 @@ -250,7 +250,7 @@
   7.107               of NONE => semicolon [
   7.108                      (str o deresolve_base) classparam,
   7.109                      str "=",
   7.110 -                    pr_app tyvars thm false init_syms NOBR (c_inst, [])
   7.111 +                    pr_app tyvars thm init_syms NOBR (c_inst, [])
   7.112                    ]
   7.113                | SOME (k, pr) =>
   7.114                    let
   7.115 @@ -266,9 +266,9 @@
   7.116                        (*dictionaries are not relevant at this late stage*)
   7.117                    in
   7.118                      semicolon [
   7.119 -                      pr_term tyvars thm false vars NOBR lhs,
   7.120 +                      pr_term tyvars thm vars NOBR lhs,
   7.121                        str "=",
   7.122 -                      pr_term tyvars thm false vars NOBR rhs
   7.123 +                      pr_term tyvars thm vars NOBR rhs
   7.124                      ]
   7.125                    end;
   7.126            in
   7.127 @@ -463,10 +463,10 @@
   7.128        | pr_monad pr_bind pr (SOME (bind, false), t) vars = vars
   7.129            |> pr_bind NOBR bind
   7.130            |>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]);
   7.131 -    fun pretty pr naming thm pat vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
   7.132 +    fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
   7.133       of SOME (bind, t') => let
   7.134            val (binds, t'') = implode_monad ((the o Code_Thingol.lookup_const naming) c_bind) t'
   7.135 -          val (ps, vars') = fold_map (pr_monad (pr_haskell_bind (K (K pr)) thm) pr) (bind :: binds) vars;
   7.136 +          val (ps, vars') = fold_map (pr_monad (pr_haskell_bind (K pr) thm) pr) (bind :: binds) vars;
   7.137          in (brackify fxy o single o Pretty.enclose "do {" "}" o Pretty.breaks) (ps @| pr vars' NOBR t'') end
   7.138        | NONE => brackify_infix (1, L) fxy
   7.139            [pr vars (INFX (1, L)) t1, str ">>=", pr vars (INFX (1, X)) t2]
     8.1 --- a/src/Tools/code/code_ml.ML	Tue Oct 28 17:53:46 2008 +0100
     8.2 +++ b/src/Tools/code/code_ml.ML	Wed Oct 29 11:33:40 2008 +0100
     8.3 @@ -83,40 +83,40 @@
     8.4           of NONE => pr_tycoexpr fxy (tyco, tys)
     8.5            | SOME (i, pr) => pr pr_typ fxy tys)
     8.6        | pr_typ fxy (ITyVar v) = str ("'" ^ v);
     8.7 -    fun pr_term thm pat vars fxy (IConst c) =
     8.8 -          pr_app thm pat vars fxy (c, [])
     8.9 -      | pr_term thm pat vars fxy (IVar v) =
    8.10 +    fun pr_term thm vars fxy (IConst c) =
    8.11 +          pr_app thm vars fxy (c, [])
    8.12 +      | pr_term thm vars fxy (IVar v) =
    8.13            str (Code_Name.lookup_var vars v)
    8.14 -      | pr_term thm pat vars fxy (t as t1 `$ t2) =
    8.15 +      | pr_term thm vars fxy (t as t1 `$ t2) =
    8.16            (case Code_Thingol.unfold_const_app t
    8.17 -           of SOME c_ts => pr_app thm pat vars fxy c_ts
    8.18 +           of SOME c_ts => pr_app thm vars fxy c_ts
    8.19              | NONE =>
    8.20 -                brackify fxy [pr_term thm pat vars NOBR t1, pr_term thm pat vars BR t2])
    8.21 -      | pr_term thm pat vars fxy (t as _ `|-> _) =
    8.22 +                brackify fxy [pr_term thm vars NOBR t1, pr_term thm vars BR t2])
    8.23 +      | pr_term thm vars fxy (t as _ `|-> _) =
    8.24            let
    8.25              val (binds, t') = Code_Thingol.unfold_abs t;
    8.26              fun pr ((v, pat), ty) =
    8.27                pr_bind thm NOBR ((SOME v, pat), ty)
    8.28                #>> (fn p => concat [str "fn", p, str "=>"]);
    8.29              val (ps, vars') = fold_map pr binds vars;
    8.30 -          in brackets (ps @ [pr_term thm pat vars' NOBR t']) end
    8.31 -      | pr_term thm pat vars fxy (ICase (cases as (_, t0))) =
    8.32 +          in brackets (ps @ [pr_term thm vars' NOBR t']) end
    8.33 +      | pr_term thm vars fxy (ICase (cases as (_, t0))) =
    8.34            (case Code_Thingol.unfold_const_app t0
    8.35             of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
    8.36                  then pr_case thm vars fxy cases
    8.37 -                else pr_app thm pat vars fxy c_ts
    8.38 +                else pr_app thm vars fxy c_ts
    8.39              | NONE => pr_case thm vars fxy cases)
    8.40 -    and pr_app' thm pat vars (app as ((c, (iss, tys)), ts)) =
    8.41 +    and pr_app' thm vars (app as ((c, (iss, tys)), ts)) =
    8.42        if is_cons c then let
    8.43          val k = length tys
    8.44        in if k < 2 then 
    8.45 -        (str o deresolve) c :: map (pr_term thm pat vars BR) ts
    8.46 +        (str o deresolve) c :: map (pr_term thm vars BR) ts
    8.47        else if k = length ts then
    8.48 -        [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term thm pat vars NOBR) ts)]
    8.49 -      else [pr_term thm pat vars BR (Code_Thingol.eta_expand k app)] end else
    8.50 +        [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term thm vars NOBR) ts)]
    8.51 +      else [pr_term thm vars BR (Code_Thingol.eta_expand k app)] end else
    8.52          (str o deresolve) c
    8.53 -          :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts
    8.54 -    and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons naming thm pat vars
    8.55 +          :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm vars BR) ts
    8.56 +    and pr_app thm vars = gen_pr_app pr_app' pr_term syntax_const naming thm vars
    8.57      and pr_bind' ((NONE, NONE), _) = str "_"
    8.58        | pr_bind' ((SOME v, NONE), _) = str v
    8.59        | pr_bind' ((NONE, SOME p), _) = p
    8.60 @@ -128,12 +128,12 @@
    8.61              fun pr ((pat, ty), t) vars =
    8.62                vars
    8.63                |> pr_bind thm NOBR ((NONE, SOME pat), ty)
    8.64 -              |>> (fn p => semicolon [str "val", p, str "=", pr_term thm false vars NOBR t])
    8.65 +              |>> (fn p => semicolon [str "val", p, str "=", pr_term thm vars NOBR t])
    8.66              val (ps, vars') = fold_map pr binds vars;
    8.67            in
    8.68              Pretty.chunks [
    8.69                [str ("let"), Pretty.fbrk, Pretty.chunks ps] |> Pretty.block,
    8.70 -              [str ("in"), Pretty.fbrk, pr_term thm false vars' NOBR t'] |> Pretty.block,
    8.71 +              [str ("in"), Pretty.fbrk, pr_term thm vars' NOBR t'] |> Pretty.block,
    8.72                str ("end")
    8.73              ]
    8.74            end
    8.75 @@ -143,12 +143,12 @@
    8.76                let
    8.77                  val (p, vars') = pr_bind thm NOBR ((NONE, SOME pat), ty) vars;
    8.78                in
    8.79 -                concat [str delim, p, str "=>", pr_term thm false vars' NOBR t]
    8.80 +                concat [str delim, p, str "=>", pr_term thm vars' NOBR t]
    8.81                end;
    8.82            in
    8.83              (Pretty.enclose "(" ")" o single o brackify fxy) (
    8.84                str "case"
    8.85 -              :: pr_term thm false vars NOBR td
    8.86 +              :: pr_term thm vars NOBR td
    8.87                :: pr "of" b
    8.88                :: map (pr "|") bs
    8.89              )
    8.90 @@ -209,8 +209,8 @@
    8.91                               then [str ":", pr_typ NOBR ty]
    8.92                               else
    8.93                                 pr_tyvar_dicts vs_dict
    8.94 -                               @ map (pr_term thm true vars BR) ts)
    8.95 -                       @ [str "=", pr_term thm false vars NOBR t]
    8.96 +                               @ map (pr_term thm vars BR) ts)
    8.97 +                       @ [str "=", pr_term thm vars NOBR t]
    8.98                          )
    8.99                        end
   8.100                    in
   8.101 @@ -303,7 +303,7 @@
   8.102                concat [
   8.103                  (str o pr_label_classparam) classparam,
   8.104                  str "=",
   8.105 -                pr_app thm false reserved_names NOBR (c_inst, [])
   8.106 +                pr_app thm reserved_names NOBR (c_inst, [])
   8.107                ];
   8.108            in
   8.109              semicolon ([
   8.110 @@ -376,38 +376,38 @@
   8.111           of NONE => pr_tycoexpr fxy (tyco, tys)
   8.112            | SOME (i, pr) => pr pr_typ fxy tys)
   8.113        | pr_typ fxy (ITyVar v) = str ("'" ^ v);
   8.114 -    fun pr_term thm pat vars fxy (IConst c) =
   8.115 -          pr_app thm pat vars fxy (c, [])
   8.116 -      | pr_term thm pat vars fxy (IVar v) =
   8.117 +    fun pr_term thm vars fxy (IConst c) =
   8.118 +          pr_app thm vars fxy (c, [])
   8.119 +      | pr_term thm vars fxy (IVar v) =
   8.120            str (Code_Name.lookup_var vars v)
   8.121 -      | pr_term thm pat vars fxy (t as t1 `$ t2) =
   8.122 +      | pr_term thm vars fxy (t as t1 `$ t2) =
   8.123            (case Code_Thingol.unfold_const_app t
   8.124 -           of SOME c_ts => pr_app thm pat vars fxy c_ts
   8.125 +           of SOME c_ts => pr_app thm vars fxy c_ts
   8.126              | NONE =>
   8.127 -                brackify fxy [pr_term thm pat vars NOBR t1, pr_term thm pat vars BR t2])
   8.128 -      | pr_term thm pat vars fxy (t as _ `|-> _) =
   8.129 +                brackify fxy [pr_term thm vars NOBR t1, pr_term thm vars BR t2])
   8.130 +      | pr_term thm vars fxy (t as _ `|-> _) =
   8.131            let
   8.132              val (binds, t') = Code_Thingol.unfold_abs t;
   8.133              fun pr ((v, pat), ty) = pr_bind thm BR ((SOME v, pat), ty);
   8.134              val (ps, vars') = fold_map pr binds vars;
   8.135 -          in brackets (str "fun" :: ps @ str "->" @@ pr_term thm pat vars' NOBR t') end
   8.136 -      | pr_term thm pat vars fxy (ICase (cases as (_, t0))) = (case Code_Thingol.unfold_const_app t0
   8.137 +          in brackets (str "fun" :: ps @ str "->" @@ pr_term thm vars' NOBR t') end
   8.138 +      | pr_term thm vars fxy (ICase (cases as (_, t0))) = (case Code_Thingol.unfold_const_app t0
   8.139             of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
   8.140                  then pr_case thm vars fxy cases
   8.141 -                else pr_app thm pat vars fxy c_ts
   8.142 +                else pr_app thm vars fxy c_ts
   8.143              | NONE => pr_case thm vars fxy cases)
   8.144 -    and pr_app' thm pat vars (app as ((c, (iss, tys)), ts)) =
   8.145 +    and pr_app' thm vars (app as ((c, (iss, tys)), ts)) =
   8.146        if is_cons c then
   8.147          if length tys = length ts
   8.148          then case ts
   8.149           of [] => [(str o deresolve) c]
   8.150 -          | [t] => [(str o deresolve) c, pr_term thm pat vars BR t]
   8.151 +          | [t] => [(str o deresolve) c, pr_term thm vars BR t]
   8.152            | _ => [(str o deresolve) c, Pretty.enum "," "(" ")"
   8.153 -                    (map (pr_term thm pat vars NOBR) ts)]
   8.154 -        else [pr_term thm pat vars BR (Code_Thingol.eta_expand (length tys) app)]
   8.155 +                    (map (pr_term thm vars NOBR) ts)]
   8.156 +        else [pr_term thm vars BR (Code_Thingol.eta_expand (length tys) app)]
   8.157        else (str o deresolve) c
   8.158 -        :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts)
   8.159 -    and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons naming thm pat vars
   8.160 +        :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm vars BR) ts)
   8.161 +    and pr_app thm vars = gen_pr_app pr_app' pr_term syntax_const naming thm vars
   8.162      and pr_bind' ((NONE, NONE), _) = str "_"
   8.163        | pr_bind' ((SOME v, NONE), _) = str v
   8.164        | pr_bind' ((NONE, SOME p), _) = p
   8.165 @@ -420,19 +420,19 @@
   8.166                vars
   8.167                |> pr_bind thm NOBR ((NONE, SOME pat), ty)
   8.168                |>> (fn p => concat
   8.169 -                  [str "let", p, str "=", pr_term thm false vars NOBR t, str "in"])
   8.170 +                  [str "let", p, str "=", pr_term thm vars NOBR t, str "in"])
   8.171              val (ps, vars') = fold_map pr binds vars;
   8.172 -          in Pretty.chunks (ps @| pr_term thm false vars' NOBR t') end
   8.173 +          in Pretty.chunks (ps @| pr_term thm vars' NOBR t') end
   8.174        | pr_case thm vars fxy (((td, ty), b::bs), _) =
   8.175            let
   8.176              fun pr delim (pat, t) =
   8.177                let
   8.178                  val (p, vars') = pr_bind thm NOBR ((NONE, SOME pat), ty) vars;
   8.179 -              in concat [str delim, p, str "->", pr_term thm false vars' NOBR t] end;
   8.180 +              in concat [str delim, p, str "->", pr_term thm vars' NOBR t] end;
   8.181            in
   8.182              (Pretty.enclose "(" ")" o single o brackify fxy) (
   8.183                str "match"
   8.184 -              :: pr_term thm false vars NOBR td
   8.185 +              :: pr_term thm vars NOBR td
   8.186                :: pr "with" b
   8.187                :: map (pr "|") bs
   8.188              )
   8.189 @@ -464,9 +464,9 @@
   8.190                    |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
   8.191                        (insert (op =)) ts []);
   8.192                in concat [
   8.193 -                (Pretty.block o Pretty.commas) (map (pr_term thm true vars NOBR) ts),
   8.194 +                (Pretty.block o Pretty.commas) (map (pr_term thm vars NOBR) ts),
   8.195                  str "->",
   8.196 -                pr_term thm false vars NOBR t
   8.197 +                pr_term thm vars NOBR t
   8.198                ] end;
   8.199              fun pr_eqs name ty [] =
   8.200                    let
   8.201 @@ -493,9 +493,9 @@
   8.202                            (insert (op =)) ts []);
   8.203                    in
   8.204                      concat (
   8.205 -                      map (pr_term thm true vars BR) ts
   8.206 +                      map (pr_term thm vars BR) ts
   8.207                        @ str "="
   8.208 -                      @@ pr_term thm false vars NOBR t
   8.209 +                      @@ pr_term thm vars NOBR t
   8.210                      )
   8.211                    end
   8.212                | pr_eqs _ _ (eqs as (eq as (([_], _), _)) :: eqs') =
   8.213 @@ -615,7 +615,7 @@
   8.214                concat [
   8.215                  (str o deresolve) classparam,
   8.216                  str "=",
   8.217 -                pr_app thm false reserved_names NOBR (c_inst, [])
   8.218 +                pr_app thm reserved_names NOBR (c_inst, [])
   8.219                ];
   8.220            in
   8.221              concat (
     9.1 --- a/src/Tools/code/code_printer.ML	Tue Oct 28 17:53:46 2008 +0100
     9.2 +++ b/src/Tools/code/code_printer.ML	Wed Oct 29 11:33:40 2008 +0100
     9.3 @@ -43,12 +43,12 @@
     9.4      -> fixity -> 'a list -> Pretty.T)) option * OuterParse.token list
     9.5    val simple_const_syntax: (int * ((fixity -> iterm -> Pretty.T)
     9.6      -> fixity -> (iterm * itype) list -> Pretty.T)) option -> const_syntax option
     9.7 -  val gen_pr_app: (thm -> bool -> Code_Name.var_ctxt -> const * iterm list -> Pretty.T list)
     9.8 -    -> (thm -> bool -> Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
     9.9 -    -> (string -> const_syntax option) -> (string -> bool) -> Code_Thingol.naming
    9.10 -    -> thm -> bool -> Code_Name.var_ctxt -> fixity -> const * iterm list -> Pretty.T
    9.11 +  val gen_pr_app: (thm -> Code_Name.var_ctxt -> const * iterm list -> Pretty.T list)
    9.12 +    -> (thm -> Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
    9.13 +    -> (string -> const_syntax option) -> Code_Thingol.naming
    9.14 +    -> thm -> Code_Name.var_ctxt -> fixity -> const * iterm list -> Pretty.T
    9.15    val gen_pr_bind: ((string option * Pretty.T option) * itype -> Pretty.T)
    9.16 -    -> (thm -> bool -> Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
    9.17 +    -> (thm -> Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
    9.18      -> thm -> fixity
    9.19      -> (string option * iterm option) * itype -> Code_Name.var_ctxt -> Pretty.T * Code_Name.var_ctxt
    9.20  
    9.21 @@ -127,26 +127,23 @@
    9.22  type tyco_syntax = int * ((fixity -> itype -> Pretty.T)
    9.23    -> fixity -> itype list -> Pretty.T);
    9.24  type const_syntax = int * ((Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
    9.25 -  -> Code_Thingol.naming -> thm -> bool -> Code_Name.var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
    9.26 +  -> Code_Thingol.naming -> thm -> Code_Name.var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
    9.27  
    9.28  fun simple_const_syntax x = (Option.map o apsnd)
    9.29 -  (fn pretty => fn pr => fn naming => fn thm => fn pat => fn vars => pretty (pr vars)) x;
    9.30 +  (fn pretty => fn pr => fn naming => fn thm => fn vars => pretty (pr vars)) x;
    9.31  
    9.32 -fun gen_pr_app pr_app pr_term syntax_const is_cons naming thm pat
    9.33 -    vars fxy (app as ((c, (_, tys)), ts)) =
    9.34 +fun gen_pr_app pr_app pr_term syntax_const naming thm vars fxy (app as ((c, (_, tys)), ts)) =
    9.35    case syntax_const c
    9.36 -   of NONE => if pat andalso not (is_cons c) then
    9.37 -        nerror thm "Non-constructor in pattern"
    9.38 -        else brackify fxy (pr_app thm pat vars app)
    9.39 +   of NONE => brackify fxy (pr_app thm vars app)
    9.40      | SOME (k, pr) =>
    9.41          let
    9.42 -          fun pr' fxy ts = pr (pr_term thm pat) naming thm pat vars fxy (ts ~~ curry Library.take k tys);
    9.43 +          fun pr' fxy ts = pr (pr_term thm) naming thm vars fxy (ts ~~ curry Library.take k tys);
    9.44          in if k = length ts
    9.45            then pr' fxy ts
    9.46          else if k < length ts
    9.47            then case chop k ts of (ts1, ts2) =>
    9.48 -            brackify fxy (pr' APP ts1 :: map (pr_term thm pat vars BR) ts2)
    9.49 -          else pr_term thm pat vars fxy (Code_Thingol.eta_expand k app)
    9.50 +            brackify fxy (pr' APP ts1 :: map (pr_term thm vars BR) ts2)
    9.51 +          else pr_term thm vars fxy (Code_Thingol.eta_expand k app)
    9.52          end;
    9.53  
    9.54  fun gen_pr_bind pr_bind pr_term thm (fxy : fixity) ((v, pat), ty : itype) vars =
    9.55 @@ -157,7 +154,7 @@
    9.56      val vars' = Code_Name.intro_vars (the_list v) vars;
    9.57      val vars'' = Code_Name.intro_vars vs vars';
    9.58      val v' = Option.map (Code_Name.lookup_var vars') v;
    9.59 -    val pat' = Option.map (pr_term thm true vars'' fxy) pat;
    9.60 +    val pat' = Option.map (pr_term thm vars'' fxy) pat;
    9.61    in (pr_bind ((v', pat'), ty), vars'') end;
    9.62  
    9.63  
    10.1 --- a/src/Tools/code/code_thingol.ML	Tue Oct 28 17:53:46 2008 +0100
    10.2 +++ b/src/Tools/code/code_thingol.ML	Wed Oct 29 11:33:40 2008 +0100
    10.3 @@ -667,6 +667,11 @@
    10.4        | is_undefined _ = false;
    10.5      fun mk_case (co, n) t =
    10.6        let
    10.7 +        val _ = if (is_some o Code.get_datatype_of_constr thy) co then ()
    10.8 +          else error ("Non-constructor " ^ quote co
    10.9 +            ^ " encountered in case pattern"
   10.10 +            ^ (case thm of NONE => ""
   10.11 +              | SOME thm => ", in equation\n" ^ Display.string_of_thm thm))
   10.12          val (vs, body) = Term.strip_abs_eta n t;
   10.13          val selector = list_comb (Const (co, map snd vs ---> dty), map Free vs);
   10.14        in if is_undefined body then NONE else SOME (selector, body) end;