src/Pure/Proof/proof_syntax.ML
changeset 15574 b1d1b5bfc464
parent 15570 8d8c70b41bab
child 16182 a5c77d298ad7
     1.1 --- a/src/Pure/Proof/proof_syntax.ML	Fri Mar 04 11:44:26 2005 +0100
     1.2 +++ b/src/Pure/Proof/proof_syntax.ML	Fri Mar 04 15:07:34 2005 +0100
     1.3 @@ -97,10 +97,10 @@
     1.4  
     1.5      val tab = Symtab.foldl (fn (tab, (key, ps)) =>
     1.6        let val prop = getOpt (assoc (thms', key), Bound 0)
     1.7 -      in fst (Library.foldr (fn ((prop', prf), x as (tab, i)) =>
     1.8 +      in fst (foldr (fn ((prop', prf), x as (tab, i)) =>
     1.9          if prop <> prop' then
    1.10            (Symtab.update ((key ^ "_" ^ string_of_int i, prf), tab), i+1)
    1.11 -        else x) (ps, (tab, 1)))
    1.12 +        else x) (tab, 1) ps)
    1.13        end) (Symtab.empty, thms);
    1.14  
    1.15      fun rename (Abst (s, T, prf)) = Abst (s, T, rename prf)