equal
deleted
inserted
replaced
367 (* read = parse + check *) |
367 (* read = parse + check *) |
368 |
368 |
369 fun read_sort ctxt = parse_sort ctxt #> check_sort ctxt; |
369 fun read_sort ctxt = parse_sort ctxt #> check_sort ctxt; |
370 fun read_typ ctxt = parse_typ ctxt #> singleton (check_typs ctxt); |
370 fun read_typ ctxt = parse_typ ctxt #> singleton (check_typs ctxt); |
371 |
371 |
372 fun read_terms ctxt = map (parse_term ctxt) #> check_terms ctxt; |
372 fun read_terms ctxt = Par_List.map_name "Syntax.read_terms" (parse_term ctxt) #> check_terms ctxt; |
373 fun read_props ctxt = map (parse_prop ctxt) #> check_props ctxt; |
373 fun read_props ctxt = Par_List.map_name "Syntax.read_props" (parse_prop ctxt) #> check_props ctxt; |
374 |
374 |
375 val read_term = singleton o read_terms; |
375 val read_term = singleton o read_terms; |
376 val read_prop = singleton o read_props; |
376 val read_prop = singleton o read_props; |
377 |
377 |
378 val read_sort_global = read_sort o Proof_Context.init_global; |
378 val read_sort_global = read_sort o Proof_Context.init_global; |