src/Pure/theory.ML
changeset 16991 39f5760f72d7
parent 16944 83ea7e3c6ec9
child 17038 6dbd7c63a5a6
     1.1 --- a/src/Pure/theory.ML	Mon Aug 01 19:20:44 2005 +0200
     1.2 +++ b/src/Pure/theory.ML	Mon Aug 01 19:20:45 2005 +0200
     1.3 @@ -207,7 +207,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 (Term.compress_term o Logic.varify) o prep_axm thy) raw_axms;
     1.8 +    val axms = map (apsnd (Compress.term thy o Logic.varify) o prep_axm thy) raw_axms;
     1.9      val axioms' = NameSpace.extend_table (Sign.naming_of thy) (axioms, axms)
    1.10        handle Symtab.DUPS dups => err_dup_axms dups;
    1.11    in axioms' end);
    1.12 @@ -303,9 +303,9 @@
    1.13      val _ = check_overloading thy overloaded const;
    1.14    in
    1.15      defs
    1.16 -    |> Defs.declare (declared const)
    1.17 -    |> fold (Defs.declare o declared) rhs_consts
    1.18 -    |> Defs.define pp const (Sign.full_name thy bname) rhs_consts
    1.19 +    |> Defs.declare thy (declared const)
    1.20 +    |> fold (Defs.declare thy o declared) rhs_consts
    1.21 +    |> Defs.define thy const (Sign.full_name thy bname) rhs_consts
    1.22    end
    1.23    handle ERROR => error (Pretty.string_of (Pretty.block
    1.24     [Pretty.str ("The error(s) above occurred in definition " ^ quote bname ^ ":"),
    1.25 @@ -338,7 +338,7 @@
    1.26  fun gen_add_finals prep_term overloaded raw_terms thy =
    1.27    let
    1.28      val pp = Sign.pp thy;
    1.29 -    fun finalize tm finals =
    1.30 +    fun finalize tm =
    1.31        let
    1.32          val _ = no_vars pp tm;
    1.33          val const as (c, _) =
    1.34 @@ -346,8 +346,8 @@
    1.35            | Free _ => error "Attempt to finalize variable (or undeclared constant)"
    1.36            | _ => error "Attempt to finalize non-constant term")
    1.37            |> check_overloading thy overloaded;
    1.38 -      in finals |> Defs.declare (c, Sign.the_const_type thy c) |> Defs.finalize const end;
    1.39 -  in thy |> map_defs (fold finalize (map (prep_term thy) raw_terms)) end;
    1.40 +      in Defs.declare thy (c, Sign.the_const_type thy c) #> Defs.finalize thy const end;
    1.41 +  in thy |> map_defs (fold (finalize o prep_term thy) raw_terms) end;
    1.42  
    1.43  fun read_term thy = Sign.simple_read_term thy TypeInfer.logicT;
    1.44  fun cert_term thy = #1 o Sign.certify_term (Sign.pp thy) thy;