src/HOL/Nominal/nominal_fresh_fun.ML
changeset 59621 291934bac95e
parent 59586 ddf6deaadfe8
child 59635 025f70f35daf
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -23,8 +23,8 @@
     1.4        (head_of (Logic.incr_indexes (Ts, j) t),
     1.5         fold_rev Term.abs ps u)) tinst;
     1.6      val th' = instf
     1.7 -      (map (apply2 (Thm.ctyp_of thy)) tyinst')
     1.8 -      (map (apply2 (Thm.cterm_of thy)) tinst')
     1.9 +      (map (apply2 (Thm.global_ctyp_of thy)) tyinst')
    1.10 +      (map (apply2 (Thm.global_cterm_of thy)) tinst')
    1.11        (Thm.lift_rule cgoal th)
    1.12    in
    1.13      compose_tac ctxt (elim, th', Thm.nprems_of th) i st
    1.14 @@ -149,7 +149,7 @@
    1.15         val thy = Thm.theory_of_thm st;
    1.16     in case subtract (op =) vars vars' of
    1.17       [x] =>
    1.18 -      Seq.single (Thm.instantiate ([], [(Thm.cterm_of thy x, Thm.cterm_of thy (fold_rev Term.abs params (Bound 0)))]) st)
    1.19 +      Seq.single (Thm.instantiate ([], [(Thm.global_cterm_of thy x, Thm.global_cterm_of thy (fold_rev Term.abs params (Bound 0)))]) st)
    1.20      | _ => error "fresh_fun_simp: Too many variables, please report."
    1.21     end
    1.22    in