Compress.term;
authorwenzelm
Mon Aug 01 19:20:45 2005 +0200 (2005-08-01)
changeset 1699139f5760f72d7
parent 16990 7fceb965cf52
child 16992 38bb4f03a887
Compress.term;
src/Pure/theory.ML
src/Pure/thm.ML
     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;
     2.1 --- a/src/Pure/thm.ML	Mon Aug 01 19:20:44 2005 +0200
     2.2 +++ b/src/Pure/thm.ML	Mon Aug 01 19:20:45 2005 +0200
     2.3 @@ -573,13 +573,15 @@
     2.4  (*Compression of theorems -- a separate rule, not integrated with the others,
     2.5    as it could be slow.*)
     2.6  fun compress (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
     2.7 -  Thm {thy_ref = thy_ref,
     2.8 -    der = der,
     2.9 -    maxidx = maxidx,
    2.10 -    shyps = shyps,
    2.11 -    hyps = map Term.compress_term hyps,
    2.12 -    tpairs = map (pairself Term.compress_term) tpairs,
    2.13 -    prop = Term.compress_term prop};
    2.14 +  let val thy = Theory.deref thy_ref in
    2.15 +    Thm {thy_ref = thy_ref,
    2.16 +      der = der,
    2.17 +      maxidx = maxidx,
    2.18 +      shyps = shyps,
    2.19 +      hyps = map (Compress.term thy) hyps,
    2.20 +      tpairs = map (pairself (Compress.term thy)) tpairs,
    2.21 +      prop = Compress.term thy prop}
    2.22 +  end;
    2.23  
    2.24  fun adjust_maxidx_thm (Thm {thy_ref, der, shyps, hyps, tpairs, prop, ...}) =
    2.25    Thm {thy_ref = thy_ref,
    2.26 @@ -1310,7 +1312,7 @@
    2.27          (*unknowns appearing elsewhere be preserved!*)
    2.28          val vids = map (#1 o #1 o dest_Var) vars;
    2.29          fun rename(t as Var((x,i),T)) =
    2.30 -                (case assoc(al,x) of
    2.31 +                (case assoc_string (al,x) of
    2.32                     SOME(y) => if x mem_string vids orelse y mem_string vids then t
    2.33                                else Var((y,i),T)
    2.34                   | NONE=> t)