1.1 --- a/src/Pure/sign.ML	Fri Nov 09 19:37:35 2007 +0100
     1.2 +++ b/src/Pure/sign.ML	Fri Nov 09 19:37:35 2007 +0100
     1.3 @@ -610,13 +610,13 @@
     1.4  
     1.5  (* add type abbreviations *)
     1.6  
     1.7 -fun gen_add_tyabbr prep_typ (a, vs, rhs, mx) thy =
     1.8 +fun gen_add_tyabbr parse_typ (a, vs, rhs, mx) thy =
     1.9    thy |> map_sign (fn (naming, syn, tsig, consts) =>
    1.10      let
    1.11 +      val ctxt = ProofContext.init thy;
    1.12        val syn' = Syntax.extend_type_gram [(a, length vs, mx)] syn;
    1.13        val a' = Syntax.type_name a mx;
    1.14 -      val abbr = (a', vs,
    1.15 -          certify_typ_mode Type.mode_syntax thy (prep_typ (ProofContext.init thy) rhs))
    1.16 +      val abbr = (a', vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
    1.17          handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote a');
    1.18        val tsig' = Type.add_abbrevs naming [abbr] tsig;
    1.19      in (naming, syn', tsig', consts) end);
    1.20 @@ -627,10 +627,10 @@
    1.21  
    1.22  (* modify syntax *)
    1.23  
    1.24 -fun gen_syntax change_gram prep_typ mode args thy =
    1.25 +fun gen_syntax change_gram parse_typ mode args thy =
    1.26    let
    1.27 -    fun prep (c, T, mx) = (c,
    1.28 -        certify_typ_mode Type.mode_syntax thy (prep_typ (ProofContext.init thy) T), mx)
    1.29 +    val ctxt = ProofContext.init thy;
    1.30 +    fun prep (c, T, mx) = (c, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt T), mx)
    1.31        handle ERROR msg =>
    1.32          cat_error msg ("in syntax declaration " ^ quote (Syntax.const_name c mx));
    1.33    in thy |> map_syn (change_gram (is_logtype thy) mode (map prep args)) end;
    1.34 @@ -655,9 +655,10 @@
    1.35  
    1.36  local
    1.37  
    1.38 -fun gen_add_consts prep_typ authentic tags raw_args thy =
    1.39 +fun gen_add_consts parse_typ authentic tags raw_args thy =
    1.40    let
    1.41 -    val prepT = Type.no_tvars o Term.no_dummyT o prep_typ thy;
    1.42 +    val ctxt = ProofContext.init thy;
    1.43 +    val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
    1.44      fun prep (raw_c, raw_T, raw_mx) =
    1.45        let
    1.46          val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
    1.47 @@ -677,10 +678,10 @@
    1.48  
    1.49  in
    1.50  
    1.51 -val add_consts = snd oo gen_add_consts read_typ false [];
    1.52 -val add_consts_i = snd oo gen_add_consts certify_typ false [];
    1.53 +val add_consts = snd oo gen_add_consts Syntax.parse_typ false [];
    1.54 +val add_consts_i = snd oo gen_add_consts (K I) false [];
    1.55  
    1.56 -fun declare_const tags arg = gen_add_consts certify_typ true tags [arg] #>> the_single;
    1.57 +fun declare_const tags arg = gen_add_consts (K I) true tags [arg] #>> the_single;
    1.58  
    1.59  end;
    1.60