src/Pure/sign.ML
changeset 24517 eaed6ac5f7f2
parent 24485 687bbb686ef9
child 24674 4ade7ac6a21c
equal deleted inserted replaced
24516:c121834a8808 24517:eaed6ac5f7f2
   565 
   565 
   566 fun read_def_terms'
   566 fun read_def_terms'
   567     pp is_logtype syn consts map_free ctxt (def_type, def_sort) used freeze raw_args =
   567     pp is_logtype syn consts map_free ctxt (def_type, def_sort) used freeze raw_args =
   568   let
   568   let
   569     val thy = ProofContext.theory_of ctxt;
   569     val thy = ProofContext.theory_of ctxt;
   570     val check_typs = Syntax.check_typs (Type.set_mode Type.mode_default ctxt);
   570     fun check_typs Ts = map (certify_typ thy) Ts
       
   571       handle TYPE (msg, _, _) => error msg;
   571 
   572 
   572     fun infer args = TypeInfer.infer_types pp (tsig_of thy) check_typs
   573     fun infer args = TypeInfer.infer_types pp (tsig_of thy) check_typs
   573         (try (Consts.the_constraint consts)) def_type used freeze args |>> map fst
   574         (try (Consts.the_constraint consts)) def_type used freeze args |>> map fst
   574       handle TYPE (msg, _, _) => error msg;
   575       handle TYPE (msg, _, _) => error msg;
   575 
   576