src/Pure/sign.ML
changeset 36610 bafd82950e24
parent 36450 62eaaffe6e47
child 37145 01aa36932739
     1.1 --- a/src/Pure/sign.ML	Mon May 03 07:59:51 2010 +0200
     1.2 +++ b/src/Pure/sign.ML	Mon May 03 14:25:56 2010 +0200
     1.3 @@ -361,7 +361,7 @@
     1.4  
     1.5  fun gen_syntax change_gram parse_typ mode args thy =
     1.6    let
     1.7 -    val ctxt = ProofContext.init thy;
     1.8 +    val ctxt = ProofContext.init_global thy;
     1.9      fun prep (c, T, mx) = (c, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt T), mx)
    1.10        handle ERROR msg => cat_error msg ("in syntax declaration " ^ quote c);
    1.11    in thy |> map_syn (change_gram (is_logtype thy) mode (map prep args)) end;
    1.12 @@ -398,7 +398,7 @@
    1.13  
    1.14  fun gen_add_consts parse_typ raw_args thy =
    1.15    let
    1.16 -    val ctxt = ProofContext.init thy;
    1.17 +    val ctxt = ProofContext.init_global thy;
    1.18      val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
    1.19      fun prep (b, raw_T, mx) =
    1.20        let
    1.21 @@ -497,7 +497,7 @@
    1.22  
    1.23  fun gen_trrules f args thy = thy |> map_syn (fn syn =>
    1.24    let val rules = map (Syntax.map_trrule (apfst (intern_type thy))) args
    1.25 -  in f (ProofContext.init thy) (is_logtype thy) syn rules syn end);
    1.26 +  in f (ProofContext.init_global thy) (is_logtype thy) syn rules syn end);
    1.27  
    1.28  val add_trrules = gen_trrules Syntax.update_trrules;
    1.29  val del_trrules = gen_trrules Syntax.remove_trrules;