src/ZF/Tools/typechk.ML
changeset 16458 4c6fd0c01d28
parent 15570 8d8c70b41bab
child 16800 90eff1b52428
     1.1 --- a/src/ZF/Tools/typechk.ML	Fri Jun 17 18:33:42 2005 +0200
     1.2 +++ b/src/ZF/Tools/typechk.ML	Fri Jun 17 18:35:27 2005 +0200
     1.3 @@ -124,33 +124,26 @@
     1.4  (** global tcset **)
     1.5  
     1.6  structure TypecheckingArgs =
     1.7 -  struct
     1.8 +struct
     1.9    val name = "ZF/type-checker";
    1.10    type T = tcset ref;
    1.11    val empty = ref (TC{rules=[], net=Net.empty});
    1.12    fun copy (ref tc) = ref tc;
    1.13 -  val prep_ext = copy;
    1.14 -  fun merge (ref tc1, ref tc2) = ref (merge_tc (tc1, tc2));
    1.15 +  val extend = copy;
    1.16 +  fun merge _ (ref tc1, ref tc2) = ref (merge_tc (tc1, tc2));
    1.17    fun print _ (ref tc) = print_tc tc;
    1.18 -  end;
    1.19 +end;
    1.20  
    1.21  structure TypecheckingData = TheoryDataFun(TypecheckingArgs);
    1.22  
    1.23  val print_tcset = TypecheckingData.print;
    1.24 -val tcset_ref_of_sg = TypecheckingData.get_sg;
    1.25  val tcset_ref_of = TypecheckingData.get;
    1.26 -
    1.27 -
    1.28 -(* access global tcset *)
    1.29 +val tcset_of = ! o tcset_ref_of;
    1.30 +val tcset = tcset_of o Context.the_context;
    1.31 +val tcset_ref = tcset_ref_of o Context.the_context;
    1.32  
    1.33 -val tcset_of_sg = ! o tcset_ref_of_sg;
    1.34 -val tcset_of = tcset_of_sg o sign_of;
    1.35 -
    1.36 -val tcset = tcset_of o Context.the_context;
    1.37 -val tcset_ref = tcset_ref_of_sg o sign_of o Context.the_context;
    1.38 -
    1.39 -fun TCSET tacf st = tacf (tcset_of_sg (Thm.sign_of_thm st)) st;
    1.40 -fun TCSET' tacf i st = tacf (tcset_of_sg (Thm.sign_of_thm st)) i st;
    1.41 +fun TCSET tacf st = tacf (tcset_of (Thm.theory_of_thm st)) st;
    1.42 +fun TCSET' tacf i st = tacf (tcset_of (Thm.theory_of_thm st)) i st;
    1.43  
    1.44  
    1.45  (* change global tcset *)
    1.46 @@ -168,15 +161,14 @@
    1.47  
    1.48  (** local tcset **)
    1.49  
    1.50 -structure LocalTypecheckingArgs =
    1.51 -struct
    1.52 +structure LocalTypecheckingData = ProofDataFun
    1.53 +(struct
    1.54    val name = TypecheckingArgs.name;
    1.55    type T = tcset;
    1.56    val init = tcset_of;
    1.57    fun print _ tcset = print_tc tcset;
    1.58 -end;
    1.59 +end);
    1.60  
    1.61 -structure LocalTypecheckingData = ProofDataFun(LocalTypecheckingArgs);
    1.62  val local_tcset_of = LocalTypecheckingData.get;
    1.63  
    1.64