src/Pure/theory.ML
changeset 26631 d6b6c74a8bcf
parent 25059 e6e0ee56a672
child 26668 65023d4fd226
     1.1 --- a/src/Pure/theory.ML	Sat Apr 12 17:00:43 2008 +0200
     1.2 +++ b/src/Pure/theory.ML	Sat Apr 12 17:00:45 2008 +0200
     1.3 @@ -211,7 +211,7 @@
     1.4  
     1.5  fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms =>
     1.6    let
     1.7 -    val axms = map (apsnd (Compress.term thy o Logic.varify) o prep_axm thy) raw_axms;
     1.8 +    val axms = map (apsnd Logic.varify o prep_axm thy) raw_axms;
     1.9      val axioms' = NameSpace.extend_table (Sign.naming_of thy) axms axioms
    1.10        handle Symtab.DUP dup => err_dup_axm dup;
    1.11    in axioms' end);
    1.12 @@ -235,7 +235,7 @@
    1.13      val consts = Sign.consts_of thy;
    1.14      fun prep const =
    1.15        let val Const (c, T) = Sign.no_vars pp (Const const)
    1.16 -      in (c, Consts.typargs consts (c, Compress.typ thy (Logic.varifyT T))) end;
    1.17 +      in (c, Consts.typargs consts (c, Logic.varifyT T)) end;
    1.18  
    1.19      val lhs_vars = Term.add_tfreesT (#2 lhs) [];
    1.20      val rhs_extras = fold (#2 #> Term.fold_atyps (fn TFree v =>