src/Pure/Isar/element.ML
changeset 20304 500a3373c93c
parent 20264 f09a4003e12d
child 20548 8ef25fe585a8
     1.1 --- a/src/Pure/Isar/element.ML	Wed Aug 02 22:26:57 2006 +0200
     1.2 +++ b/src/Pure/Isar/element.ML	Wed Aug 02 22:26:58 2006 +0200
     1.3 @@ -354,13 +354,15 @@
     1.4  
     1.5  fun rename_thm ren th =
     1.6    let
     1.7 -    val subst = Drule.frees_of th
     1.8 -      |> map_filter (fn (x, T) =>
     1.9 +    val thy = Thm.theory_of_thm th;
    1.10 +    val subst = (Drule.fold_terms o Term.fold_aterms)
    1.11 +      (fn Free (x, T) =>
    1.12          let val x' = rename ren x
    1.13 -        in if x = x' then NONE else SOME ((x, T), (Free (x', T))) end);
    1.14 +        in if x = x' then I else insert (eq_fst (op =)) ((x, T), Free (x', T)) end
    1.15 +      | _ => I) th [];
    1.16    in
    1.17      if null subst then th
    1.18 -    else th |> hyps_rule (instantiate_frees (Thm.theory_of_thm th) subst)
    1.19 +    else th |> hyps_rule (instantiate_frees thy subst)
    1.20    end;
    1.21  
    1.22  fun rename_witness ren =
    1.23 @@ -381,13 +383,11 @@
    1.24    if Symtab.is_empty env then I
    1.25    else Term.map_term_types (instT_type env);
    1.26  
    1.27 -fun instT_subst env th =
    1.28 -  Drule.tfrees_of th
    1.29 -  |> map_filter (fn (a, S) =>
    1.30 -    let
    1.31 -      val T = TFree (a, S);
    1.32 -      val T' = the_default T (Symtab.lookup env a);
    1.33 -    in if T = T' then NONE else SOME (a, T') end);
    1.34 +fun instT_subst env th = (Drule.fold_terms o Term.fold_types o Term.fold_atyps)
    1.35 +  (fn T as TFree (a, _) =>
    1.36 +    let val T' = the_default T (Symtab.lookup env a)
    1.37 +    in if T = T' then I else insert (op =) (a, T') end
    1.38 +  | _ => I) th [];
    1.39  
    1.40  fun instT_thm thy env th =
    1.41    if Symtab.is_empty env then th
    1.42 @@ -425,13 +425,14 @@
    1.43    else
    1.44      let
    1.45        val substT = instT_subst envT th;
    1.46 -      val subst = Drule.frees_of th
    1.47 -        |> map_filter (fn (x, T) =>
    1.48 +      val subst = (Drule.fold_terms o Term.fold_aterms)
    1.49 +       (fn Free (x, T) =>
    1.50            let
    1.51              val T' = instT_type envT T;
    1.52              val t = Free (x, T');
    1.53              val t' = the_default t (Symtab.lookup env x);
    1.54 -          in if t aconv t' then NONE else SOME ((x, T'), t') end);
    1.55 +          in if t aconv t' then I else insert (eq_fst (op =)) ((x, T'), t') end
    1.56 +       | _ => I) th [];
    1.57      in
    1.58        if null substT andalso null subst then th
    1.59        else th |> hyps_rule