src/HOL/Tools/split_rule.ML
changeset 59621 291934bac95e
parent 59582 0fbed69ff081
child 60362 befdc10ebb42
     1.1 --- a/src/HOL/Tools/split_rule.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/Tools/split_rule.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -42,7 +42,7 @@
     1.4  fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2]))) rl =
     1.5        let val T' = HOLogic.flatten_tupleT T1 ---> T2;
     1.6            val newt = ap_split T1 T2 (Var (v, T'));
     1.7 -          val cterm = Thm.cterm_of (Thm.theory_of_thm rl);
     1.8 +          val cterm = Thm.global_cterm_of (Thm.theory_of_thm rl);
     1.9        in Thm.instantiate ([], [(cterm t, cterm newt)]) rl end
    1.10    | split_rule_var' _ rl = rl;
    1.11  
    1.12 @@ -56,7 +56,7 @@
    1.13  
    1.14  fun complete_split_rule_var (t as Var (v, T), ts) (rl, vs) =
    1.15        let
    1.16 -        val cterm = Thm.cterm_of (Thm.theory_of_thm rl)
    1.17 +        val cterm = Thm.global_cterm_of (Thm.theory_of_thm rl)
    1.18          val (Us', U') = strip_type T;
    1.19          val Us = take (length ts) Us';
    1.20          val U = drop (length ts) Us' ---> U';
    1.21 @@ -70,7 +70,7 @@
    1.22                end
    1.23            | mk_tuple _ x = x;
    1.24          val newt = ap_split' Us U (Var (v, T'));
    1.25 -        val cterm = Thm.cterm_of (Thm.theory_of_thm rl);
    1.26 +        val cterm = Thm.global_cterm_of (Thm.theory_of_thm rl);
    1.27          val (vs', insts) = fold mk_tuple ts (vs, []);
    1.28        in
    1.29          (Drule.instantiate_normalize ([], [(cterm t, cterm newt)] @ insts) rl, vs')