src/Pure/proof_general.ML
changeset 15992 cb02d70a2040
parent 15985 f00dd5e06ffe
child 16022 96a9bf7ac18d
equal deleted inserted replaced
15991:670f8e4b5a98 15992:cb02d70a2040
   141 fun var_or_skolem s =
   141 fun var_or_skolem s =
   142   (case Syntax.read_variable s of
   142   (case Syntax.read_variable s of
   143     SOME (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
       
   147           (setmp show_question_marks true Syntax.string_of_vname (x', i)))
   147   | NONE => tagit var_tag s);
   148   | NONE => tagit var_tag s);
   148 
   149 
   149 val proof_general_trans =
   150 val proof_general_trans =
   150  Syntax.tokentrans_mode proof_generalN
   151  Syntax.tokentrans_mode proof_generalN
   151   [("class", tagit class_tag),
   152   [("class", tagit class_tag),