src/Pure/Isar/constdefs.ML
changeset 36610 bafd82950e24
parent 35845 e5980f0ad025
child 36865 7330e4eefbd7
     1.1 --- a/src/Pure/Isar/constdefs.ML	Mon May 03 07:59:51 2010 +0200
     1.2 +++ b/src/Pure/Isar/constdefs.ML	Mon May 03 14:25:56 2010 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4  
     1.5      fun err msg ts = error (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts));
     1.6  
     1.7 -    val thy_ctxt = ProofContext.init thy;
     1.8 +    val thy_ctxt = ProofContext.init_global thy;
     1.9      val struct_ctxt = #2 (ProofContext.add_fixes structs thy_ctxt);
    1.10      val ((d, mx), var_ctxt) =
    1.11        (case raw_decl of
    1.12 @@ -62,7 +62,7 @@
    1.13  
    1.14  fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy =
    1.15    let
    1.16 -    val ctxt = ProofContext.init thy;
    1.17 +    val ctxt = ProofContext.init_global thy;
    1.18      val (structs, _) = prep_vars (map (fn (x, T) => (x, T, Structure)) raw_structs) ctxt;
    1.19      val (decls, thy') = fold_map (gen_constdef prep_vars prep_prop prep_att structs) specs thy;
    1.20    in Pretty.writeln (Proof_Display.pretty_consts ctxt (K true) decls); thy' end;