src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 36610 bafd82950e24
parent 36160 f84fa49a0b69
child 36692 54b64d4ad524
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon May 03 07:59:51 2010 +0200
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon May 03 14:25:56 2010 +0200
     1.3 @@ -71,7 +71,7 @@
     1.4  end;
     1.5  
     1.6  fun legacy_infer_term thy t =
     1.7 -  let val ctxt = ProofContext.set_mode ProofContext.mode_schematic (ProofContext.init thy)
     1.8 +  let val ctxt = ProofContext.set_mode ProofContext.mode_schematic (ProofContext.init_global thy)
     1.9    in singleton (Syntax.check_terms ctxt) (intern_term thy t) end;
    1.10  
    1.11  fun pg'' thy defs t tacs =
    1.12 @@ -347,7 +347,7 @@
    1.13  
    1.14  (* ----- theorems concerning finiteness and induction ----------------------- *)
    1.15  
    1.16 -  val global_ctxt = ProofContext.init thy;
    1.17 +  val global_ctxt = ProofContext.init_global thy;
    1.18  
    1.19    val _ = trace " Proving ind...";
    1.20    val ind =
    1.21 @@ -422,7 +422,7 @@
    1.22            bot :: map (fn (c,_) => Long_Name.base_name c) cons;
    1.23    in adms @ flat (map2 one_eq bottoms eqs) end;
    1.24  
    1.25 -val inducts = Project_Rule.projections (ProofContext.init thy) ind;
    1.26 +val inducts = Project_Rule.projections (ProofContext.init_global thy) ind;
    1.27  fun ind_rule (dname, rule) =
    1.28      ((Binding.empty, [rule]),
    1.29       [Rule_Cases.case_names case_ns, Induct.induct_type dname]);
    1.30 @@ -470,7 +470,7 @@
    1.31  local
    1.32  
    1.33    fun legacy_infer_term thy t =
    1.34 -      singleton (Syntax.check_terms (ProofContext.init thy)) (intern_term thy t);
    1.35 +      singleton (Syntax.check_terms (ProofContext.init_global thy)) (intern_term thy t);
    1.36    fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t);
    1.37    fun infer_props thy = map (apsnd (legacy_infer_prop thy));
    1.38    fun add_defs_i x = PureThy.add_defs false (map Thm.no_attributes x);