src/HOL/Tools/datatype_codegen.ML
changeset 21516 c2a116a2c4fd
parent 21454 a1937c51ed88
child 21546 268b6bed0cc8
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Fri Nov 24 17:23:15 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Fri Nov 24 22:05:12 2006 +0100
     1.3 @@ -380,13 +380,15 @@
     1.4    val rew_conj = thm "HOL.atomize_conj" |> Thm.symmetric;
     1.5    val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
     1.6    val not_eq_quodlibet = thm "not_eq_quodlibet";
     1.7 -in fun get_cert_datatype thy dtco =
     1.8 +in
     1.9 +
    1.10 +fun get_cert_datatype thy dtco =
    1.11    let
    1.12      val SOME (vs, cs) = DatatypePackage.get_datatype_spec thy dtco;
    1.13      val inject = (#inject o DatatypePackage.the_datatype thy) dtco
    1.14        |> map (fn thm => bool_eq_implies OF [thm] )
    1.15        |> map (Tactic.rewrite_rule [rew_eq, rew_conj]);
    1.16 -    val ctxt = Context.init_proof thy;
    1.17 +    val ctxt = ProofContext.init thy;
    1.18      val simpset = Simplifier.context ctxt
    1.19        (MetaSimplifier.empty_ss addsimprocs [DatatypePackage.distinct_simproc]);
    1.20      val cos = map (fn (co, tys) =>
    1.21 @@ -398,12 +400,15 @@
    1.22        |> map (fn t => Goal.prove_global thy [] [] t (K tac))
    1.23        |> map (fn thm => not_eq_quodlibet OF [thm])
    1.24    in inject @ distinct end
    1.25 -end (*local*);
    1.26 +
    1.27 +end;
    1.28  
    1.29  local
    1.30    val not_sym = thm "HOL.not_sym";
    1.31    val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
    1.32 -in fun get_eq_datatype thy dtco =
    1.33 +in
    1.34 +
    1.35 +fun get_eq_datatype thy dtco =
    1.36    let
    1.37      val SOME (vs, cs) = DatatypePackage.get_datatype_spec thy dtco;
    1.38      fun mk_triv_inject co =
    1.39 @@ -418,7 +423,7 @@
    1.40        in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) HOL.refl] end;
    1.41      val inject1 = map_filter (fn (co, []) => SOME (mk_triv_inject co) | _ => NONE) cs
    1.42      val inject2 = (#inject o DatatypePackage.the_datatype thy) dtco;
    1.43 -    val ctxt = Context.init_proof thy;
    1.44 +    val ctxt = ProofContext.init thy;
    1.45      val simpset = Simplifier.context ctxt
    1.46        (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]);
    1.47      val cos = map (fn (co, tys) =>
    1.48 @@ -430,7 +435,8 @@
    1.49        |> map (fn t => Goal.prove_global thy [] [] t (K tac))
    1.50        |> (fn thms => thms @ map (fn thm => not_sym OF [thm]) thms)
    1.51    in inject1 @ inject2 @ distinct end;
    1.52 -end (*local*);
    1.53 +
    1.54 +end;
    1.55  
    1.56  fun add_datatype_case_const dtco thy =
    1.57    let