src/HOL/Tools/Datatype/datatype_data.ML
changeset 42359 6ca5407863ed
parent 42297 140f283266b7
child 42361 23f352990944
     1.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Sat Apr 16 13:48:45 2011 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Sat Apr 16 15:25:25 2011 +0200
     1.3 @@ -378,12 +378,13 @@
     1.4  
     1.5  fun gen_rep_datatype prep_term config after_qed alt_names raw_ts thy =
     1.6    let
     1.7 +    val ctxt = ProofContext.init_global thy;
     1.8 +
     1.9      fun constr_of_term (Const (c, T)) = (c, T)
    1.10 -      | constr_of_term t =
    1.11 -          error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
    1.12 -    fun no_constr (c, T) = error ("Bad constructor: "
    1.13 -      ^ Sign.extern_const thy c ^ "::"
    1.14 -      ^ Syntax.string_of_typ_global thy T);
    1.15 +      | constr_of_term t = error ("Not a constant: " ^ Syntax.string_of_term ctxt t);
    1.16 +    fun no_constr (c, T) =
    1.17 +      error ("Bad constructor: " ^ ProofContext.extern_const ctxt c ^ "::" ^
    1.18 +        Syntax.string_of_typ ctxt T);
    1.19      fun type_of_constr (cT as (_, T)) =
    1.20        let
    1.21          val frees = OldTerm.typ_tfrees T;
    1.22 @@ -437,8 +438,7 @@
    1.23          #-> after_qed
    1.24        end;
    1.25    in
    1.26 -    thy
    1.27 -    |> ProofContext.init_global
    1.28 +    ctxt
    1.29      |> Proof.theorem NONE after_qed' ((map o map) (rpair []) (flat rules))
    1.30    end;
    1.31