src/HOL/Tools/record.ML
changeset 59621 291934bac95e
parent 59617 b60e65ad13df
child 59642 929984c529d3
     1.1 --- a/src/HOL/Tools/record.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -78,7 +78,7 @@
     1.4      fun match name ((name', _), _) = name = name';
     1.5      fun getvar name =
     1.6        (case find_first (match name) (Term.add_vars (Thm.prop_of thm) []) of
     1.7 -        SOME var => Thm.cterm_of (Thm.theory_of_thm thm) (Var var)
     1.8 +        SOME var => Thm.global_cterm_of (Thm.theory_of_thm thm) (Var var)
     1.9        | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm]));
    1.10    in
    1.11      cterm_instantiate (map (apfst getvar) values) thm
    1.12 @@ -97,7 +97,7 @@
    1.13    let
    1.14      val exists_thm =
    1.15        UNIV_I
    1.16 -      |> Drule.instantiate' [SOME (Thm.ctyp_of thy (Logic.varifyT_global rep_type))] [];
    1.17 +      |> Drule.instantiate' [SOME (Thm.global_ctyp_of thy (Logic.varifyT_global rep_type))] [];
    1.18      val proj_constr = Abs_inverse OF [exists_thm];
    1.19      val absT = Type (tyco, map TFree vs);
    1.20    in
    1.21 @@ -141,7 +141,7 @@
    1.22      (*construct a type and body for the isomorphism constant by
    1.23        instantiating the theorem to which the definition will be applied*)
    1.24      val intro_inst =
    1.25 -      rep_inject RS named_cterm_instantiate [("abst", Thm.cterm_of typ_thy absC)] iso_tuple_intro;
    1.26 +      rep_inject RS named_cterm_instantiate [("abst", Thm.global_cterm_of typ_thy absC)] iso_tuple_intro;
    1.27      val (_, body) = Logic.dest_equals (List.last (Thm.prems_of intro_inst));
    1.28      val isomT = fastype_of body;
    1.29      val isom_binding = Binding.suffix_name isoN b;
    1.30 @@ -1121,7 +1121,7 @@
    1.31  
    1.32  fun get_upd_acc_cong_thm upd acc thy ss =
    1.33    let
    1.34 -    val insts = [("upd", Thm.cterm_of thy upd), ("ac", Thm.cterm_of thy acc)];
    1.35 +    val insts = [("upd", Thm.global_cterm_of thy upd), ("ac", Thm.global_cterm_of thy acc)];
    1.36      val prop = Thm.concl_of (named_cterm_instantiate insts updacc_cong_triv);
    1.37    in
    1.38      Goal.prove (Proof_Context.init_global thy) [] [] prop
    1.39 @@ -1375,9 +1375,9 @@
    1.40  
    1.41      fun mk_split_free_tac free induct_thm i =
    1.42        let
    1.43 -        val cfree = Thm.cterm_of thy free;
    1.44 +        val cfree = Thm.global_cterm_of thy free;
    1.45          val _$ (_ $ r) = Thm.concl_of induct_thm;
    1.46 -        val crec = Thm.cterm_of thy r;
    1.47 +        val crec = Thm.global_cterm_of thy r;
    1.48          val thm = cterm_instantiate [(crec, cfree)] induct_thm;
    1.49        in
    1.50          simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms induct_atomize}) i THEN
    1.51 @@ -1473,7 +1473,7 @@
    1.52        | [x] => (head_of x, false));
    1.53      val rule'' =
    1.54        cterm_instantiate
    1.55 -        (map (apply2 (Proof_Context.cterm_of ctxt))
    1.56 +        (map (apply2 (Thm.cterm_of ctxt))
    1.57            (case rev params of
    1.58              [] =>
    1.59                (case AList.lookup (op =) (Term.add_frees g []) s of
    1.60 @@ -1606,7 +1606,7 @@
    1.61        (roughly) the definition of the accessor.*)
    1.62      val surject = timeit_msg ctxt "record extension surjective proof:" (fn () =>
    1.63        let
    1.64 -        val cterm_ext = Thm.cterm_of defs_thy ext;
    1.65 +        val cterm_ext = Thm.global_cterm_of defs_thy ext;
    1.66          val start = named_cterm_instantiate [("y", cterm_ext)] surject_assist_idE;
    1.67          val tactic1 =
    1.68            simp_tac (put_simpset HOL_basic_ss defs_ctxt addsimps [ext_def]) 1 THEN
    1.69 @@ -1756,7 +1756,7 @@
    1.70        fun mk_eq_refl thy =
    1.71          @{thm equal_refl}
    1.72          |> Thm.instantiate
    1.73 -          ([apply2 (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
    1.74 +          ([apply2 (Thm.global_ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
    1.75          |> Axclass.unoverload thy;
    1.76        val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq);
    1.77        val ensure_exhaustive_record =
    1.78 @@ -1943,8 +1943,8 @@
    1.79                fun to_Var (Free (c, T)) = Var ((c, 1), T);
    1.80              in mk_rec (map to_Var all_vars_more) 0 end;
    1.81  
    1.82 -          val cterm_rec = Thm.cterm_of ext_thy r_rec0;
    1.83 -          val cterm_vrs = Thm.cterm_of ext_thy r_rec0_Vars;
    1.84 +          val cterm_rec = Thm.global_cterm_of ext_thy r_rec0;
    1.85 +          val cterm_vrs = Thm.global_cterm_of ext_thy r_rec0_Vars;
    1.86            val insts = [("v", cterm_rec), ("v'", cterm_vrs)];
    1.87            val init_thm = named_cterm_instantiate insts updacc_eq_triv;
    1.88            val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1;