cleanup
authorhaftmann
Sat Nov 18 00:20:29 2006 +0100 (2006-11-18)
changeset 214208b15e5e66813
parent 21419 809e7520234a
child 21421 3436c269dd23
cleanup
src/HOL/Tools/datatype_aux.ML
src/HOL/ex/Codegenerator.thy
     1.1 --- a/src/HOL/Tools/datatype_aux.ML	Sat Nov 18 00:20:28 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_aux.ML	Sat Nov 18 00:20:29 2006 +0100
     1.3 @@ -151,15 +151,15 @@
     1.4  
     1.5  fun exh_tac exh_thm_of i state =
     1.6    let
     1.7 -    val sg = Thm.sign_of_thm state;
     1.8 -    val prem = List.nth (prems_of state, i - 1);
     1.9 +    val thy = Thm.sign_of_thm state;
    1.10 +    val prem = nth (prems_of state) (i - 1);
    1.11      val params = Logic.strip_params prem;
    1.12      val (_, Type (tname, _)) = hd (rev params);
    1.13      val exhaustion = Thm.lift_rule (Thm.cprem_of state i) (exh_thm_of tname);
    1.14      val prem' = hd (prems_of exhaustion);
    1.15      val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
    1.16 -    val exhaustion' = cterm_instantiate [(cterm_of sg (head_of lhs),
    1.17 -      cterm_of sg (foldr (fn ((_, T), t) => Abs ("z", T, t))
    1.18 +    val exhaustion' = cterm_instantiate [(cterm_of thy (head_of lhs),
    1.19 +      cterm_of thy (foldr (fn ((_, T), t) => Abs ("z", T, t))
    1.20          (Bound 0) params))] exhaustion
    1.21    in compose_tac (false, exhaustion', nprems_of exhaustion) i state
    1.22    end;
     2.1 --- a/src/HOL/ex/Codegenerator.thy	Sat Nov 18 00:20:28 2006 +0100
     2.2 +++ b/src/HOL/ex/Codegenerator.thy	Sat Nov 18 00:20:29 2006 +0100
     2.3 @@ -190,7 +190,6 @@
     2.4    "Code_Generator.eq :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
     2.5    "Code_Generator.eq :: ('a\<Colon>eq) point_scheme \<Rightarrow> 'a point_scheme \<Rightarrow> bool"
     2.6  
     2.7 -code_gen (SML *)
     2.8 -code_gen (Haskell -)
     2.9 +code_gen (SML *) (Haskell -)
    2.10  
    2.11  end
    2.12 \ No newline at end of file