src/Pure/variable.ML
changeset 20797 c1f0bc7e7d80
parent 20579 4dc799edef89
child 21287 a713ae348e8a
     1.1 --- a/src/Pure/variable.ML	Sat Sep 30 20:54:34 2006 +0200
     1.2 +++ b/src/Pure/variable.ML	Sat Sep 30 21:39:17 2006 +0200
     1.3 @@ -33,7 +33,7 @@
     1.4    val add_fixes: string list -> Proof.context -> string list * Proof.context
     1.5    val add_fixes_direct: string list -> Proof.context -> Proof.context
     1.6    val fix_frees: term -> Proof.context -> Proof.context
     1.7 -  val invent_fixes: string list -> Proof.context -> string list * Proof.context
     1.8 +  val variant_fixes: string list -> Proof.context -> string list * Proof.context
     1.9    val invent_types: sort list -> Proof.context -> (string * sort) list * Proof.context
    1.10    val export_inst: Proof.context -> Proof.context -> string list * string list
    1.11    val exportT_inst: Proof.context -> Proof.context -> string list
    1.12 @@ -199,7 +199,7 @@
    1.13  
    1.14  val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type);
    1.15  
    1.16 -fun declare_thm th = fold declare_internal (Thm.full_prop_of th :: Thm.hyps_of th);
    1.17 +val declare_thm = Drule.fold_terms declare_internal;
    1.18  fun thm_context th = declare_thm th (Context.init_proof (Thm.theory_of_thm th));
    1.19  
    1.20  
    1.21 @@ -274,7 +274,7 @@
    1.22          (xs, fold Name.declare xs names));
    1.23    in ctxt |> new_fixes names' xs xs' end;
    1.24  
    1.25 -fun invent_fixes raw_xs ctxt =
    1.26 +fun variant_fixes raw_xs ctxt =
    1.27    let
    1.28      val names = names_of ctxt;
    1.29      val xs = map Name.clean raw_xs;
    1.30 @@ -360,7 +360,7 @@
    1.31      val ren = if is_open then I else Name.internal;
    1.32      val (instT, ctxt') = importT_inst ts ctxt;
    1.33      val vars = map (apsnd (TermSubst.instantiateT instT)) (rev (fold Term.add_vars ts []));
    1.34 -    val (xs, ctxt'') = invent_fixes (map (ren o #1 o #1) vars) ctxt';
    1.35 +    val (xs, ctxt'') = variant_fixes (map (ren o #1 o #1) vars) ctxt';
    1.36      val inst = vars ~~ map Free (xs ~~ map #2 vars);
    1.37    in ((instT, inst), ctxt'') end;
    1.38  
    1.39 @@ -421,7 +421,7 @@
    1.40      val t = Thm.term_of goal;
    1.41      val ps = Term.variant_frees t (Term.strip_all_vars t);   (*as they are printed :-*)
    1.42      val (xs, Ts) = split_list ps;
    1.43 -    val (xs', ctxt') = invent_fixes xs ctxt;
    1.44 +    val (xs', ctxt') = variant_fixes xs ctxt;
    1.45      val ps' = ListPair.map (cert o Free) (xs', Ts);
    1.46      val goal' = fold forall_elim_prop ps' goal;
    1.47    in ((ps', goal'), ctxt') end;