# HG changeset patch
# User haftmann
# Date 1163805629 -3600
# Node ID 8b15e5e668133f2a0599b32d922461acec870ae9
# Parent  809e7520234ac268e72127d8e4081ee695d3117a
cleanup

diff -r 809e7520234a -r 8b15e5e66813 src/HOL/Tools/datatype_aux.ML
--- a/src/HOL/Tools/datatype_aux.ML	Sat Nov 18 00:20:28 2006 +0100
+++ b/src/HOL/Tools/datatype_aux.ML	Sat Nov 18 00:20:29 2006 +0100
@@ -151,15 +151,15 @@
 
 fun exh_tac exh_thm_of i state =
   let
-    val sg = Thm.sign_of_thm state;
-    val prem = List.nth (prems_of state, i - 1);
+    val thy = Thm.sign_of_thm state;
+    val prem = nth (prems_of state) (i - 1);
     val params = Logic.strip_params prem;
     val (_, Type (tname, _)) = hd (rev params);
     val exhaustion = Thm.lift_rule (Thm.cprem_of state i) (exh_thm_of tname);
     val prem' = hd (prems_of exhaustion);
     val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
-    val exhaustion' = cterm_instantiate [(cterm_of sg (head_of lhs),
-      cterm_of sg (foldr (fn ((_, T), t) => Abs ("z", T, t))
+    val exhaustion' = cterm_instantiate [(cterm_of thy (head_of lhs),
+      cterm_of thy (foldr (fn ((_, T), t) => Abs ("z", T, t))
         (Bound 0) params))] exhaustion
   in compose_tac (false, exhaustion', nprems_of exhaustion) i state
   end;
diff -r 809e7520234a -r 8b15e5e66813 src/HOL/ex/Codegenerator.thy
--- a/src/HOL/ex/Codegenerator.thy	Sat Nov 18 00:20:28 2006 +0100
+++ b/src/HOL/ex/Codegenerator.thy	Sat Nov 18 00:20:29 2006 +0100
@@ -190,7 +190,6 @@
   "Code_Generator.eq :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
   "Code_Generator.eq :: ('a\<Colon>eq) point_scheme \<Rightarrow> 'a point_scheme \<Rightarrow> bool"
 
-code_gen (SML *)
-code_gen (Haskell -)
+code_gen (SML *) (Haskell -)
 
 end
\ No newline at end of file