src/Pure/Isar/class.ML
changeset 24707 dfeb98f84e93
parent 24701 f8bfd592a6dc
child 24731 c25aa6ae64ec
     1.1 --- a/src/Pure/Isar/class.ML	Tue Sep 25 13:28:35 2007 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Tue Sep 25 13:28:37 2007 +0200
     1.3 @@ -232,9 +232,10 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun gen_read_def thy prep_att read_def ((raw_name, raw_atts), raw_t) =
     1.8 +fun gen_read_def thy prep_att parse_prop ((raw_name, raw_atts), raw_t) =
     1.9    let
    1.10 -    val (_, t) = read_def thy (raw_name, raw_t);
    1.11 +    val ctxt = ProofContext.init thy;
    1.12 +    val t = parse_prop ctxt raw_t |> Syntax.check_prop ctxt;
    1.13      val ((c, ty), _) = Sign.cert_def (Sign.pp thy) t;
    1.14      val atts = map (prep_att thy) raw_atts;
    1.15      val insts = Consts.typargs (Sign.consts_of thy) (c, ty);
    1.16 @@ -243,7 +244,7 @@
    1.17        | _ => SOME raw_name;
    1.18    in (c, (insts, ((name, t), atts))) end;
    1.19  
    1.20 -fun read_def_cmd thy = gen_read_def thy Attrib.intern_src Theory.read_axm;
    1.21 +fun read_def_cmd thy = gen_read_def thy Attrib.intern_src Syntax.parse_prop;
    1.22  fun read_def thy = gen_read_def thy (K I) (K I);
    1.23  
    1.24  fun gen_instance prep_arity read_def do_proof raw_arities raw_defs after_qed theory =
    1.25 @@ -544,9 +545,9 @@
    1.26  
    1.27  local
    1.28  
    1.29 -fun read_param thy raw_t =
    1.30 +fun read_param thy raw_t =  (* FIXME ProofContext.read_const (!?) *)
    1.31    let
    1.32 -    val t = Sign.read_term thy raw_t
    1.33 +    val t = Syntax.read_term_global thy raw_t
    1.34    in case try dest_Const t
    1.35     of SOME (c, _) => c
    1.36      | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)