src/Pure/Isar/proof_context.ML
changeset 60924 610794dff23c
parent 60799 57dd0b45fc21
child 61168 dcdfb6355a05
equal deleted inserted replaced
60923:020becec359c 60924:610794dff23c
  1321       Facts.dest_static verbose [Global_Theory.facts_of (theory_of ctxt)] facts;
  1321       Facts.dest_static verbose [Global_Theory.facts_of (theory_of ctxt)] facts;
  1322   in
  1322   in
  1323     if null local_facts then []
  1323     if null local_facts then []
  1324     else
  1324     else
  1325       [Pretty.big_list "local facts:"
  1325       [Pretty.big_list "local facts:"
  1326         (map #1 (sort_wrt (#1 o #2) (map (`(pretty_fact ctxt)) local_facts)))]
  1326         (map #1 (sort_by (#1 o #2) (map (`(pretty_fact ctxt)) local_facts)))]
  1327   end;
  1327   end;
  1328 
  1328 
  1329 fun print_local_facts verbose ctxt =
  1329 fun print_local_facts verbose ctxt =
  1330   Pretty.writeln_chunks (pretty_local_facts verbose ctxt);
  1330   Pretty.writeln_chunks (pretty_local_facts verbose ctxt);
  1331 
  1331