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));