137 (case try Syntax.dest_skolem x of |
137 (case try Syntax.dest_skolem x of |
138 NONE => tagit free_tag x |
138 NONE => tagit free_tag x |
139 | SOME x' => tagit skolem_tag x'); |
139 | SOME x' => tagit skolem_tag x'); |
140 |
140 |
141 fun var_or_skolem s = |
141 fun var_or_skolem s = |
142 (case Syntax.read_var s of |
142 (case Syntax.read_variable s of |
143 Var ((x, i), _) => |
143 SOME (x, i) => |
144 (case try Syntax.dest_skolem x of |
144 (case try Syntax.dest_skolem x of |
145 NONE => tagit var_tag s |
145 NONE => tagit var_tag s |
146 | SOME x' => tagit skolem_tag (Syntax.string_of_vname (x', i))) |
146 | SOME x' => tagit skolem_tag (Syntax.string_of_vname (x', i))) |
147 | _ => tagit var_tag s); |
147 | NONE => tagit var_tag s); |
148 |
148 |
149 val proof_general_trans = |
149 val proof_general_trans = |
150 Syntax.tokentrans_mode proof_generalN |
150 Syntax.tokentrans_mode proof_generalN |
151 [("class", tagit class_tag), |
151 [("class", tagit class_tag), |
152 ("tfree", tagit tfree_tag), |
152 ("tfree", tagit tfree_tag), |
591 ("Setting for maximum number of premises printed", |
591 ("Setting for maximum number of premises printed", |
592 nat_option ProofContext.prems_limit)), |
592 nat_option ProofContext.prems_limit)), |
593 ("print-depth", |
593 ("print-depth", |
594 ("Setting for the ML print depth", |
594 ("Setting for the ML print depth", |
595 print_depth_option)), |
595 print_depth_option)), |
596 ("show-var-qmarks", |
596 ("show-question-marks", |
597 ("Show leading question mark of variable name", |
597 ("Show leading question mark of variable name", |
598 bool_option show_var_qmarks))]), |
598 bool_option show_question_marks))]), |
599 ("Tracing", |
599 ("Tracing", |
600 [("trace-simplifier", |
600 [("trace-simplifier", |
601 ("Trace simplification rules.", |
601 ("Trace simplification rules.", |
602 bool_option trace_simp)), |
602 bool_option trace_simp)), |
603 ("trace-rules", ("Trace application of the standard rules", |
603 ("trace-rules", ("Trace application of the standard rules", |