src/Pure/sign.ML
changeset 45427 fca432074fb2
parent 43794 49cbbe2768a8
child 45632 b23c42b9f78a
     1.1 --- a/src/Pure/sign.ML	Wed Nov 09 17:12:26 2011 +0100
     1.2 +++ b/src/Pure/sign.ML	Wed Nov 09 17:57:42 2011 +0100
     1.3 @@ -361,18 +361,18 @@
     1.4  
     1.5  fun gen_syntax change_gram parse_typ mode args thy =
     1.6    let
     1.7 -    val ctxt = Proof_Context.init_global thy;
     1.8 +    val ctxt = Type.set_mode Type.mode_syntax (Proof_Context.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  
    1.13  fun gen_add_syntax x = gen_syntax (Syntax.update_const_gram true) x;
    1.14  
    1.15 -val add_modesyntax = gen_add_syntax Syntax.parse_typ;
    1.16 +val add_modesyntax = gen_add_syntax Syntax.read_typ;
    1.17  val add_modesyntax_i = gen_add_syntax (K I);
    1.18  val add_syntax = add_modesyntax Syntax.mode_default;
    1.19  val add_syntax_i = add_modesyntax_i Syntax.mode_default;
    1.20 -val del_modesyntax = gen_syntax (Syntax.update_const_gram false) Syntax.parse_typ;
    1.21 +val del_modesyntax = gen_syntax (Syntax.update_const_gram false) Syntax.read_typ;
    1.22  val del_modesyntax_i = gen_syntax (Syntax.update_const_gram false) (K I);
    1.23  
    1.24  fun type_notation add mode args =
    1.25 @@ -396,9 +396,9 @@
    1.26  
    1.27  local
    1.28  
    1.29 -fun gen_add_consts parse_typ ctxt raw_args thy =
    1.30 +fun gen_add_consts prep_typ ctxt raw_args thy =
    1.31    let
    1.32 -    val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
    1.33 +    val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o prep_typ ctxt;
    1.34      fun prep (b, raw_T, mx) =
    1.35        let
    1.36          val c = full_name thy b;
    1.37 @@ -417,7 +417,8 @@
    1.38  in
    1.39  
    1.40  fun add_consts args thy =
    1.41 -  #2 (gen_add_consts Syntax.parse_typ (Proof_Context.init_global thy) args thy);
    1.42 +  #2 (gen_add_consts Syntax.read_typ (Proof_Context.init_global thy) args thy);
    1.43 +
    1.44  fun add_consts_i args thy =
    1.45    #2 (gen_add_consts (K I) (Proof_Context.init_global thy) args thy);
    1.46