src/HOL/Tools/Old_Datatype/old_datatype.ML
changeset 59621 291934bac95e
parent 59617 b60e65ad13df
child 59859 f9d1442c70f3
     1.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -247,9 +247,9 @@
     1.4          (thy, defs, eqns, rep_congs, dist_lemmas) =
     1.5        let
     1.6          val _ $ (_ $ (cong_f $ _) $ _) = Thm.concl_of arg_cong;
     1.7 -        val rep_const = Thm.cterm_of thy (Const (#Rep_name (#1 typedef), T --> Univ_elT));
     1.8 -        val cong' = cterm_instantiate [(Thm.cterm_of thy cong_f, rep_const)] arg_cong;
     1.9 -        val dist = cterm_instantiate [(Thm.cterm_of thy distinct_f, rep_const)] distinct_lemma;
    1.10 +        val rep_const = Thm.global_cterm_of thy (Const (#Rep_name (#1 typedef), T --> Univ_elT));
    1.11 +        val cong' = cterm_instantiate [(Thm.global_cterm_of thy cong_f, rep_const)] arg_cong;
    1.12 +        val dist = cterm_instantiate [(Thm.global_cterm_of thy distinct_f, rep_const)] distinct_lemma;
    1.13          val (thy', defs', eqns', _) =
    1.14            fold (make_constr_def typedef T (length constrs))
    1.15              (constrs ~~ constr_syntax) (Sign.add_path tname thy, defs, [], 1);
    1.16 @@ -390,7 +390,7 @@
    1.17      (* prove  inj Rep_dt_i  and  Rep_dt_i x : rep_set_dt_i *)
    1.18  
    1.19      val fun_congs =
    1.20 -      map (fn T => make_elim (Drule.instantiate' [SOME (Thm.ctyp_of thy5 T)] [] fun_cong)) branchTs;
    1.21 +      map (fn T => make_elim (Drule.instantiate' [SOME (Thm.global_ctyp_of thy5 T)] [] fun_cong)) branchTs;
    1.22  
    1.23      fun prove_iso_thms ds (inj_thms, elem_thms) =
    1.24        let
    1.25 @@ -626,7 +626,7 @@
    1.26        if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))]
    1.27        else map (Free o apfst fst o dest_Var) Ps;
    1.28      val indrule_lemma' =
    1.29 -      cterm_instantiate (map (Thm.cterm_of thy6) Ps ~~ map (Thm.cterm_of thy6) frees) indrule_lemma;
    1.30 +      cterm_instantiate (map (Thm.global_cterm_of thy6) Ps ~~ map (Thm.global_cterm_of thy6) frees) indrule_lemma;
    1.31  
    1.32      val dt_induct_prop = Old_Datatype_Prop.make_ind descr;
    1.33      val dt_induct =