src/Pure/proof_general.ML
changeset 15985 f00dd5e06ffe
parent 15964 f2074e12d1d4
child 15992 cb02d70a2040
equal deleted inserted replaced
15984:bc6ead9d6628 15985:f00dd5e06ffe
   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",