src/HOL/Nominal/nominal_fresh_fun.ML
changeset 59582 0fbed69ff081
parent 59058 a78612c67ec0
child 59586 ddf6deaadfe8
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Tue Mar 03 19:08:04 2015 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Mar 04 19:53:18 2015 +0100
     1.3 @@ -12,22 +12,22 @@
     1.4  (* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
     1.5  fun gen_res_inst_tac_term ctxt instf tyinst tinst elim th i st =
     1.6    let
     1.7 -    val thy = theory_of_thm st;
     1.8 +    val thy = Thm.theory_of_thm st;
     1.9      val cgoal = nth (cprems_of st) (i - 1);
    1.10 -    val {maxidx, ...} = rep_cterm cgoal;
    1.11 +    val {maxidx, ...} = Thm.rep_cterm cgoal;
    1.12      val j = maxidx + 1;
    1.13      val tyinst' = map (apfst (Logic.incr_tvar j)) tyinst;
    1.14 -    val ps = Logic.strip_params (term_of cgoal);
    1.15 +    val ps = Logic.strip_params (Thm.term_of cgoal);
    1.16      val Ts = map snd ps;
    1.17      val tinst' = map (fn (t, u) =>
    1.18        (head_of (Logic.incr_indexes (Ts, j) t),
    1.19         fold_rev Term.abs ps u)) tinst;
    1.20      val th' = instf
    1.21 -      (map (apply2 (ctyp_of thy)) tyinst')
    1.22 -      (map (apply2 (cterm_of thy)) tinst')
    1.23 +      (map (apply2 (Thm.ctyp_of thy)) tyinst')
    1.24 +      (map (apply2 (Thm.cterm_of thy)) tinst')
    1.25        (Thm.lift_rule cgoal th)
    1.26    in
    1.27 -    compose_tac ctxt (elim, th', nprems_of th) i st
    1.28 +    compose_tac ctxt (elim, th', Thm.nprems_of th) i st
    1.29    end handle General.Subscript => Seq.empty;
    1.30  (* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
    1.31  
    1.32 @@ -73,7 +73,7 @@
    1.33     val at_name_inst_thm = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename;
    1.34     val exists_fresh' = at_name_inst_thm RS at_exists_fresh';
    1.35  (* find the variable we want to instantiate *)
    1.36 -   val x = hd (Misc_Legacy.term_vars (prop_of exists_fresh'));
    1.37 +   val x = hd (Misc_Legacy.term_vars (Thm.prop_of exists_fresh'));
    1.38   in
    1.39     fn st =>
    1.40     (cut_inst_tac_term' ctxt [(x,s)] exists_fresh' 1 THEN
    1.41 @@ -131,7 +131,7 @@
    1.42      val simp_ctxt =
    1.43        ctxt addsimps (fresh_prod :: abs_fresh)
    1.44        addsimps fresh_perm_app;
    1.45 -    val x = hd (tl (Misc_Legacy.term_vars (prop_of exI)));
    1.46 +    val x = hd (tl (Misc_Legacy.term_vars (Thm.prop_of exI)));
    1.47      val atom_name_opt = get_inner_fresh_fun goal;
    1.48      val n = length (Logic.strip_params goal);
    1.49      (* Here we rely on the fact that the variable introduced by generate_fresh_tac *)
    1.50 @@ -145,18 +145,18 @@
    1.51      val pt_name_inst = get_dyn_thm thy ("pt_"^atom_basename^"_inst") atom_basename;
    1.52      val at_name_inst = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename;
    1.53      fun inst_fresh vars params i st =
    1.54 -   let val vars' = Misc_Legacy.term_vars (prop_of st);
    1.55 -       val thy = theory_of_thm st;
    1.56 +   let val vars' = Misc_Legacy.term_vars (Thm.prop_of st);
    1.57 +       val thy = Thm.theory_of_thm st;
    1.58     in case subtract (op =) vars vars' of
    1.59       [x] =>
    1.60 -      Seq.single (Thm.instantiate ([],[(cterm_of thy x,cterm_of thy (fold_rev Term.abs params (Bound 0)))]) st)
    1.61 +      Seq.single (Thm.instantiate ([], [(Thm.cterm_of thy x, Thm.cterm_of thy (fold_rev Term.abs params (Bound 0)))]) st)
    1.62      | _ => error "fresh_fun_simp: Too many variables, please report."
    1.63     end
    1.64    in
    1.65    ((fn st =>
    1.66    let
    1.67 -    val vars = Misc_Legacy.term_vars (prop_of st);
    1.68 -    val params = Logic.strip_params (nth (prems_of st) (i-1))
    1.69 +    val vars = Misc_Legacy.term_vars (Thm.prop_of st);
    1.70 +    val params = Logic.strip_params (nth (Thm.prems_of st) (i-1))
    1.71      (* The tactics which solve the subgoals generated
    1.72         by the conditionnal rewrite rule. *)
    1.73      val post_rewrite_tacs =