read_def_cterms (legacy version): Consts.certify;
authorwenzelm
Thu Jul 27 13:43:08 2006 +0200 (2006-07-27)
changeset 2023004cb2d917de5
parent 20229 da4ec4b48be1
child 20231 dcdd565a7fbe
read_def_cterms (legacy version): Consts.certify;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Thu Jul 27 13:43:07 2006 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu Jul 27 13:43:08 2006 +0200
     1.3 @@ -622,14 +622,19 @@
     1.4        in (Syntax.read context is_logtype syn T' s, T') end;
     1.5    in infer_types_simult pp thy consts types sorts used freeze (map read sTs) end;
     1.6  
     1.7 -fun read_def_terms (thy, types, sorts) used =
     1.8 -  read_def_terms' (pp thy) (is_logtype thy) (syn_of thy) (consts_of thy)
     1.9 -    (Context.Theory thy) (types, sorts) (Name.make_context used);
    1.10 +fun read_def_terms (thy, types, sorts) used freeze sTs =
    1.11 +  let
    1.12 +    val pp = pp thy;
    1.13 +    val consts = consts_of thy;
    1.14 +    val cert_consts = Consts.certify pp (tsig_of thy) consts;
    1.15 +    val (ts, inst) =
    1.16 +      read_def_terms' pp (is_logtype thy) (syn_of thy) consts
    1.17 +        (Context.Theory thy) (types, sorts) (Name.make_context used) freeze sTs;
    1.18 +  in (map cert_consts ts, inst) end;
    1.19  
    1.20  fun simple_read_term thy T s =
    1.21    let val ([t], _) = read_def_terms (thy, K NONE, K NONE) [] true [(s, T)]
    1.22 -  in t end
    1.23 -  handle ERROR msg => cat_error msg ("The error(s) above occurred for term " ^ s);
    1.24 +  in t end handle ERROR msg => cat_error msg ("The error(s) above occurred for term " ^ s);
    1.25  
    1.26  fun read_term thy = simple_read_term thy TypeInfer.logicT;
    1.27  fun read_prop thy = simple_read_term thy propT;