Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
authorfleury
Wed Jul 30 14:03:13 2014 +0200 (2014-07-30)
changeset 577144856a7b8b9c3
parent 57713 9e4d2f7ad0a0
child 57715 cf8e4b1acd33
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
src/HOL/ATP.thy
src/HOL/Tools/ATP/atp_proof.ML
src/HOL/Tools/ATP/atp_satallax.ML
src/HOL/Tools/SMT2/smt2_systems.ML
src/HOL/Tools/SMT2/smtlib2_isar.ML
src/HOL/Tools/SMT2/verit_isar.ML
src/HOL/Tools/SMT2/verit_proof.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
     1.1 --- a/src/HOL/ATP.thy	Wed Jul 30 14:03:13 2014 +0200
     1.2 +++ b/src/HOL/ATP.thy	Wed Jul 30 14:03:13 2014 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Automatic Theorem Provers (ATPs) *}
     1.5  
     1.6  theory ATP
     1.7 -imports Meson Hilbert_Choice
     1.8 +imports Meson
     1.9  begin
    1.10  
    1.11  subsection {* ATP problems and proofs *}
     2.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Jul 30 14:03:13 2014 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Jul 30 14:03:13 2014 +0200
     2.3 @@ -90,18 +90,17 @@
     2.4  
     2.5    val skip_term: string list -> string * string list
     2.6    val parse_thf0_formula :string list ->
     2.7 -      ('a, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term,
     2.8 -       'c) ATP_Problem.atp_formula *
     2.9 -      string list
    2.10 -  val dummy_atype :  string ATP_Problem.atp_type
    2.11 -  val role_of_tptp_string:  string -> ATP_Problem.atp_formula_role
    2.12 +    ('a, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term, 'c) ATP_Problem.atp_formula *
    2.13 +    string list
    2.14 +  val dummy_atype : string ATP_Problem.atp_type
    2.15 +  val role_of_tptp_string: string -> ATP_Problem.atp_formula_role
    2.16    val parse_line: string -> ('a * string ATP_Problem.atp_problem_line list) list ->
    2.17 -              string list -> ((string * string list) * ATP_Problem.atp_formula_role *
    2.18 -               (string, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term,
    2.19 -                'c) ATP_Problem.atp_formula
    2.20 -               * string * (string * 'd list) list) list * string list
    2.21 +    string list -> ((string * string list) * ATP_Problem.atp_formula_role *
    2.22 +    (string, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term,
    2.23 +      'c) ATP_Problem.atp_formula
    2.24 +    * string * (string * 'd list) list) list * string list
    2.25    val core_inference :   'a -> 'b -> ('b * 'b list) * ATP_Problem.atp_formula_role *
    2.26 -              ('c, 'd, (string, 'e) ATP_Problem.atp_term, 'f) ATP_Problem.atp_formula * 'a * 'g list
    2.27 +      ('c, 'd, (string, 'e) ATP_Problem.atp_term, 'f) ATP_Problem.atp_formula * 'a * 'g list
    2.28    val vampire_step_name_ord : (string * 'a) * (string * 'a) -> order
    2.29    val core_of_agsyhol_proof :  string -> string list option
    2.30  end;
    2.31 @@ -478,8 +477,8 @@
    2.32    [tptp_and, tptp_not_and, tptp_or, tptp_not_or, tptp_implies, tptp_if, tptp_iff, tptp_not_iff,
    2.33     tptp_equal, tptp_app]
    2.34  
    2.35 -fun parse_one_in_list list =
    2.36 -  foldl1 (op ||) (map Scan.this_string list)
    2.37 +fun parse_one_in_list xs =
    2.38 +  foldl1 (op ||) (map Scan.this_string xs)
    2.39  
    2.40  fun parse_binary_op x =
    2.41    (parse_one_in_list tptp_binary_ops
     3.1 --- a/src/HOL/Tools/ATP/atp_satallax.ML	Wed Jul 30 14:03:13 2014 +0200
     3.2 +++ b/src/HOL/Tools/ATP/atp_satallax.ML	Wed Jul 30 14:03:13 2014 +0200
     3.3 @@ -30,7 +30,7 @@
     3.4    ((Symbol.scan_ascii_id || ($$ "$" |-- Symbol.scan_ascii_id))
     3.5    -- Scan.option ( $$ "(" |-- Scan.option (Symbol.scan_ascii_id --| $$ ",")
     3.6    -- ((Scan.option (($$ "[" |-- (Scan.option ((scan_general_id
     3.7 -         -- Scan.repeat ($$ "," |-- scan_general_id)) >> uncurry cons) --| $$ "]"))
     3.8 +         -- Scan.repeat ($$ "," |-- scan_general_id)) >> (op ::)) --| $$ "]"))
     3.9           || (skip_term >> K "") >> (fn x => SOME [x]))
    3.10         >> (fn (SOME x) => x | NONE => NONE)) --| $$ ")"))) x
    3.11  
    3.12 @@ -39,12 +39,12 @@
    3.13  
    3.14  fun parse_prems x =
    3.15    (($$ "[" |-- parse_prem -- Scan.repeat ($$ "," |-- parse_prem) --| $$ "]")
    3.16 -     >> uncurry cons) x
    3.17 +     >> (op ::)) x
    3.18  
    3.19  fun parse_tstp_satallax_extra_arguments x =
    3.20    ($$ "," |-- scan_general_id -- (($$ "(" |-- Symbol.scan_ascii_id --| $$ "," )
    3.21    -- ($$ "[" |-- Scan.option ((parse_satallax_tstp_information
    3.22 -  -- Scan.repeat ($$ "," |-- parse_satallax_tstp_information)) >> uncurry cons)
    3.23 +  -- Scan.repeat ($$ "," |-- parse_satallax_tstp_information)) >> (op ::))
    3.24    --| $$ "]") --
    3.25    (Scan.optional ($$ "," |-- parse_prems) [] -- Scan.optional ($$ "," |-- parse_prems) []
    3.26      >> (fn (x, []) => x | (_, x) => x))
    3.27 @@ -58,7 +58,6 @@
    3.28    || (Scan.this_string "tab_inh" |-- skip_term --| $$ ".")
    3.29       >> K dummy_satallax_step) x
    3.30  
    3.31 -
    3.32  datatype satallax_step = Satallax_Step of {
    3.33    id: string,
    3.34    role: string,
    3.35 @@ -106,19 +105,23 @@
    3.36    end
    3.37  
    3.38  fun create_grouped_goal_assumption rule new_goals generated_assumptions =
    3.39 -  if length new_goals = length generated_assumptions then
    3.40 -    new_goals ~~ (map single generated_assumptions)
    3.41 -  else if 2 * length new_goals = length generated_assumptions then
    3.42 -    let
    3.43 -      fun group_by_pair (new_goal :: new_goals) (assumpt1 :: assumpt2 :: generated_assumptions) =
    3.44 -          (new_goal, [assumpt1, assumpt2]) :: group_by_pair new_goals generated_assumptions
    3.45 -        | group_by_pair [] [] = []
    3.46 -    in
    3.47 -      group_by_pair new_goals generated_assumptions
    3.48 -    end
    3.49 -  else
    3.50 -    raise Fail ("the rule " ^ rule ^" is not supported in the reconstruction.")
    3.51 -
    3.52 +  let
    3.53 +    val number_of_new_goals = length new_goals
    3.54 +    val number_of_new_assms = length generated_assumptions
    3.55 +  in
    3.56 +    if number_of_new_goals = number_of_new_assms then
    3.57 +      new_goals ~~ (map single generated_assumptions)
    3.58 +    else if 2 * number_of_new_goals = number_of_new_assms then
    3.59 +      let
    3.60 +        fun group_by_pair (new_goal :: new_goals) (assumpt1 :: assumpt2 :: generated_assumptions) =
    3.61 +            (new_goal, [assumpt1, assumpt2]) :: group_by_pair new_goals generated_assumptions
    3.62 +          | group_by_pair [] [] = []
    3.63 +      in
    3.64 +        group_by_pair new_goals generated_assumptions
    3.65 +      end
    3.66 +    else
    3.67 +      raise Fail ("the rule " ^ rule ^" is not supported in the reconstruction.")
    3.68 +  end
    3.69  fun to_satallax_step (((id, role), formula), (SOME (_,((rule, l), used_rules)))) =
    3.70      let
    3.71        val (used_assumptions, new_goals, generated_assumptions) = seperate_dependices used_rules
    3.72 @@ -173,9 +176,9 @@
    3.73        | SOME (_, th) =>
    3.74          let
    3.75            val simplified_ths_with_inlined_assumption =
    3.76 -              (case List.partition (curry tptp_term_equal th o remove_not_not) ths of
    3.77 -                ([], ths) => ATerm ((tptp_not, [dummy_atype]), [th]) :: ths
    3.78 -              | (_, _) => [])
    3.79 +            (case List.partition (curry tptp_term_equal th o remove_not_not) ths of
    3.80 +              ([], ths) => ATerm ((tptp_not, [dummy_atype]), [th]) :: ths
    3.81 +            | (_, _) => [])
    3.82          in
    3.83            find_assumptions_to_inline simplified_ths_with_inlined_assumption assms to_inline no_inline
    3.84          end))
    3.85 @@ -190,7 +193,6 @@
    3.86      | ATerm (("~", _ ), [ATerm (("$true", _), _)]) => a
    3.87      | _ => ATerm ((tptp_or, [dummy_atype]), [a, b]))) l)
    3.88  
    3.89 -
    3.90  fun get_conclusion (Satallax_Step {theorem = AAtom theorem, ...}) = theorem
    3.91  
    3.92  fun add_assumption new_used_assumptions ((Satallax_Step {id, role, theorem, assumptions,
    3.93 @@ -208,7 +210,7 @@
    3.94      fun inline_in_step (Linear_Part {node as Satallax_Step {generated_goal_assumptions,
    3.95            used_assumptions, rule, ...}, succs}) =
    3.96          if generated_goal_assumptions = [] then
    3.97 -            Linear_Part {node = node, succs = []}
    3.98 +          Linear_Part {node = node, succs = []}
    3.99          else
   3.100            let
   3.101              (*one singel goal is created, two hypothesis can be created, for the "and" rule:
   3.102 @@ -230,8 +232,8 @@
   3.103      fun inline_contradictory_assumptions (Linear_Part {node as Satallax_Step{id, theorem, ...},
   3.104         succs}) (to_inline, no_inline) =
   3.105        let
   3.106 -        val (succs, inliner) = fold_map inline_contradictory_assumptions
   3.107 -                                        succs (to_inline, (id, theorem) :: no_inline)
   3.108 +        val (succs, inliner) = fold_map inline_contradictory_assumptions succs 
   3.109 +          (to_inline, (id, theorem) :: no_inline)
   3.110        in
   3.111          (Linear_Part {node = node, succs = succs}, inliner)
   3.112        end
   3.113 @@ -239,8 +241,8 @@
   3.114          theorem = AAtom theorem, assumptions, rule, generated_goal_assumptions,
   3.115          used_assumptions, detailed_eigen}, deps}) (to_inline, no_inline) =
   3.116        let
   3.117 -        val (dep', (to_inline', no_inline')) = fold_map inline_contradictory_assumptions
   3.118 -                                                        deps (to_inline, no_inline)
   3.119 +        val (dep', (to_inline', no_inline')) = fold_map inline_contradictory_assumptions deps 
   3.120 +          (to_inline, no_inline)
   3.121          val to_inline'' =
   3.122            map (fn s => (s, get_conclusion (find_proof_step hypotheses_step s)))
   3.123              (List.filter (fn s => nth_string s 0 = "h")
   3.124 @@ -292,16 +294,16 @@
   3.125    end
   3.126  
   3.127  val satallax_known_theorems = ["eq_ind", "eq_trans2", "eq_trans3", "eq_neg_neg_id", "eq_true",
   3.128 -    "eq_and_nor", "eq_or_nand", "eq_or_imp", "eq_and_imp", "eq_imp_or", "eq_iff", "eq_sym_eq",
   3.129 -    "eq_forall_nexists", "eq_exists_nforall", "eq_leib1", "eq_leib2", "eq_leib3", "eq_leib4",
   3.130 -    "eq_eta", "SinhE", "eq_forall_Seps", "eq_SPi_Seps", "eq_exists_Seps"]
   3.131 +  "eq_and_nor", "eq_or_nand", "eq_or_imp", "eq_and_imp", "eq_imp_or", "eq_iff", "eq_sym_eq",
   3.132 +  "eq_forall_nexists", "eq_exists_nforall", "eq_leib1", "eq_leib2", "eq_leib3", "eq_leib4",
   3.133 +  "eq_eta", "SinhE", "eq_forall_Seps", "eq_SPi_Seps", "eq_exists_Seps"]
   3.134  val is_special_satallax_rule = member (op =) satallax_known_theorems
   3.135  
   3.136  fun terms_to_upper_case var (AAbs (((var', ty), b), ts)) =
   3.137 -     let
   3.138 -       val bdy = terms_to_upper_case var b
   3.139 -       val ts' = map (terms_to_upper_case var) ts
   3.140 -     in
   3.141 +    let
   3.142 +      val bdy = terms_to_upper_case var b
   3.143 +      val ts' = map (terms_to_upper_case var) ts
   3.144 +    in
   3.145        AAbs (((((var = var' ? String.implode o (map Char.toUpper) o String.explode) var'), ty),
   3.146          bdy), ts')
   3.147      end
   3.148 @@ -364,7 +366,7 @@
   3.149  fun remove_unused_dependency steps =
   3.150    let
   3.151      fun find_all_ids [] = []
   3.152 -     | find_all_ids (((id, _), _, _, _, _) :: steps) = id :: find_all_ids steps
   3.153 +      | find_all_ids (((id, _), _, _, _, _) :: steps) = id :: find_all_ids steps
   3.154      fun keep_only_used used_ids steps =
   3.155        let
   3.156          fun remove_unused (((id, ids), role, theorem, rule, deps) :: steps) =
   3.157 @@ -377,26 +379,25 @@
   3.158      keep_only_used (find_all_ids steps) steps
   3.159    end
   3.160  
   3.161 -
   3.162  fun parse_proof local_name problem =
   3.163 -    strip_spaces_except_between_idents
   3.164 -    #> raw_explode
   3.165 -    #>
   3.166 -      (if local_name <> satallaxN then
   3.167 -        (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
   3.168 -          (Scan.finite Symbol.stopper (Scan.repeat1 (parse_line local_name problem) >> flat)))
   3.169 -           #> fst)
   3.170 -      else
   3.171 -        (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
   3.172 -          (Scan.finite Symbol.stopper (Scan.repeat1 (parse_tstp_thf0_satallax_line))))
   3.173 -            #> fst
   3.174 -            #> rev
   3.175 -            #> map to_satallax_step
   3.176 -            #> seperate_assumptions_and_steps
   3.177 -            #> create_satallax_proof_graph
   3.178 -            #> add_quantifier_in_tree_part [] []
   3.179 -            #> transform_to_standard_atp_step []
   3.180 -            #> remove_unused_dependency))
   3.181 +  strip_spaces_except_between_idents
   3.182 +  #> raw_explode
   3.183 +  #>
   3.184 +    (if local_name <> satallaxN then
   3.185 +      (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
   3.186 +        (Scan.finite Symbol.stopper (Scan.repeat1 (parse_line local_name problem) >> flat)))
   3.187 +         #> fst)
   3.188 +    else
   3.189 +      (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
   3.190 +        (Scan.finite Symbol.stopper (Scan.repeat1 (parse_tstp_thf0_satallax_line))))
   3.191 +        #> fst
   3.192 +        #> rev
   3.193 +        #> map to_satallax_step
   3.194 +        #> seperate_assumptions_and_steps
   3.195 +        #> create_satallax_proof_graph
   3.196 +        #> add_quantifier_in_tree_part [] []
   3.197 +        #> transform_to_standard_atp_step []
   3.198 +        #> remove_unused_dependency))
   3.199  
   3.200  fun atp_proof_of_tstplike_proof _ _ "" = []
   3.201    | atp_proof_of_tstplike_proof local_prover problem tstp =
     4.1 --- a/src/HOL/Tools/SMT2/smt2_systems.ML	Wed Jul 30 14:03:13 2014 +0200
     4.2 +++ b/src/HOL/Tools/SMT2/smt2_systems.ML	Wed Jul 30 14:03:13 2014 +0200
     4.3 @@ -105,7 +105,7 @@
     4.4    smt_options = [],
     4.5    default_max_relevant = 120 (* FUDGE *),
     4.6    outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat"
     4.7 -              "warning : proof_done: status is still open"),
     4.8 +    "warning : proof_done: status is still open"),
     4.9    parse_proof = SOME VeriT_Proof_Parse.parse_proof,
    4.10    replay = NONE }
    4.11  
     5.1 --- a/src/HOL/Tools/SMT2/smtlib2_isar.ML	Wed Jul 30 14:03:13 2014 +0200
     5.2 +++ b/src/HOL/Tools/SMT2/smtlib2_isar.ML	Wed Jul 30 14:03:13 2014 +0200
     5.3 @@ -59,7 +59,7 @@
     5.4      and un_term t = map_aterms un_free t
     5.5    in un_term end
     5.6  
     5.7 -(* It is not entirely clear if this is necessary for abstractions variables. *)
     5.8 +(* It is not entirely clear why this should be necessary, especially for abstractions variables. *)
     5.9  val unskolemize_names =
    5.10    Term.map_abs_vars (perhaps (try Name.dest_skolem))
    5.11    #> Term.map_aterms (perhaps (try (fn Free (s, T) => Free (Name.dest_skolem s, T))))
     6.1 --- a/src/HOL/Tools/SMT2/verit_isar.ML	Wed Jul 30 14:03:13 2014 +0200
     6.2 +++ b/src/HOL/Tools/SMT2/verit_isar.ML	Wed Jul 30 14:03:13 2014 +0200
     6.3 @@ -27,7 +27,6 @@
     6.4      conjecture_id fact_helper_ids proof =
     6.5    let
     6.6      val thy = Proof_Context.theory_of ctxt
     6.7 -
     6.8      fun steps_of (VeriT_Proof.VeriT_Step {id, rule, prems, concl, ...}) =
     6.9        let
    6.10          val concl' = postprocess_step_conclusion concl thy rewrite_rules ll_defs
    6.11 @@ -45,6 +44,8 @@
    6.12              [(name0, role0, concl0, rule, []),
    6.13               ((id, []), Plain, concl', veriT_rewrite_rule,
    6.14                name0 :: normalizing_prems ctxt concl0)] end
    6.15 +        else if rule = veriT_tmp_ite_elim_rule then
    6.16 +          [standard_step Lemma]
    6.17          else
    6.18            [standard_step Plain]
    6.19        end
     7.1 --- a/src/HOL/Tools/SMT2/verit_proof.ML	Wed Jul 30 14:03:13 2014 +0200
     7.2 +++ b/src/HOL/Tools/SMT2/verit_proof.ML	Wed Jul 30 14:03:13 2014 +0200
     7.3 @@ -22,6 +22,8 @@
     7.4    val veriT_step_prefix : string
     7.5    val veriT_input_rule: string
     7.6    val veriT_rewrite_rule : string
     7.7 +  val veriT_tmp_skolemize_rule : string
     7.8 +  val veriT_tmp_ite_elim_rule : string
     7.9  end;
    7.10  
    7.11  structure VeriT_Proof: VERIT_PROOF =
    7.12 @@ -85,6 +87,14 @@
    7.13       replace_bound_var_by_free_var v free_vars
    7.14    | replace_bound_var_by_free_var u _ = u
    7.15  
    7.16 +fun replace_bound_all_by_ex ((q as Const (_, typ)) $ Abs (var, ty, u)) free_var =
    7.17 +    (case List.find (fn v => String.isPrefix v var) free_var of
    7.18 +      NONE => q $ Abs (var, ty, replace_bound_all_by_ex u free_var)
    7.19 +    | SOME _ => Const (@{const_name "HOL.Ex"}, typ) $ Abs (var, ty, replace_bound_all_by_ex u free_var))
    7.20 +  | replace_bound_all_by_ex (u $ v) free_vars = replace_bound_all_by_ex u free_vars $
    7.21 +     replace_bound_all_by_ex v free_vars
    7.22 +  | replace_bound_all_by_ex u _ = u
    7.23 +
    7.24  fun find_type_in_formula (Abs(v, ty, u)) var_name =
    7.25      if String.isPrefix var_name v then SOME ty else find_type_in_formula u var_name
    7.26    | find_type_in_formula (u $ v) var_name =
    7.27 @@ -195,7 +205,7 @@
    7.28      #> fix_subproof_steps
    7.29      ##> to_node
    7.30      #> (fn (subproof, (step, cx)) => (subproof @ [step], cx))
    7.31 -    #> (fn (steps, cx) => fold_map update_step_and_cx steps cx)
    7.32 +    #> uncurry (fold_map update_step_and_cx)
    7.33    end
    7.34  
    7.35  
    7.36 @@ -236,8 +246,8 @@
    7.37  
    7.38  (*Yes every case is possible: the introduced var is not on a special size of the equality sign.*)
    7.39  fun find_ite_var_in_term (Const ("HOL.If", _) $ _ $
    7.40 -      (Const ("HOL.eq", _) $ Free (var1, _) $ Free (var2, _) ) $
    7.41 -      (Const ("HOL.eq", _) $ Free (var3, _) $ Free (var4, _) )) =
    7.42 +      (Const (@{const_name "HOL.eq"}, _) $ Free (var1, _) $ Free (var2, _) ) $
    7.43 +      (Const (@{const_name "HOL.eq"}, _) $ Free (var3, _) $ Free (var4, _) )) =
    7.44      let
    7.45        fun get_number_of_ite_transformed_var var =
    7.46          perhaps (try (unprefix "ite")) var
    7.47 @@ -278,7 +288,7 @@
    7.48  
    7.49  
    7.50  fun correct_veriT_step steps (st as VeriT_Node {id, rule, prems, concl, bounds}) =
    7.51 -  if rule = "tmp_ite_elim" then
    7.52 +  if rule = veriT_tmp_ite_elim_rule then
    7.53      if bounds = [] then
    7.54        (*if the introduced var has already been defined,
    7.55          adding the definition as a dependency*)
    7.56 @@ -325,7 +335,7 @@
    7.57      val smtlib2_lines_without_at =
    7.58        remove_all_at (map SMTLIB2.parse (seperate_into_steps lines))
    7.59      val (u, env) = apfst flat (fold_map (fn l => fn cx => parse_proof_step cx l)
    7.60 -                             smtlib2_lines_without_at (empty_context ctxt typs funs))
    7.61 +      smtlib2_lines_without_at (empty_context ctxt typs funs))
    7.62      val t = correct_veriT_steps u
    7.63      fun node_to_step (VeriT_Node {id, rule, prems, concl, bounds, ...}) =
    7.64        mk_step id rule prems concl bounds
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 30 14:03:13 2014 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 30 14:03:13 2014 +0200
     8.3 @@ -66,7 +66,7 @@
     8.4      zipperposition_cnf_rule]
     8.5  
     8.6  val is_skolemize_rule = member (op =) skolemize_rules
     8.7 -val is_arith_rule = (String.isPrefix z3_th_lemma_rule) orf (member (op =) veriT_arith_rules)
     8.8 +val is_arith_rule = String.isPrefix z3_th_lemma_rule orf member (op =) veriT_arith_rules
     8.9  val is_datatype_rule = String.isPrefix spass_pirate_datatype_rule
    8.10  
    8.11  fun raw_label_of_num num = (num, 0)
    8.12 @@ -84,8 +84,7 @@
    8.13        line :: lines
    8.14      else if t aconv @{prop True} then
    8.15        map (replace_dependencies_in_line (name, [])) lines
    8.16 -    else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule
    8.17 -        orelse is_skolemize_rule rule then
    8.18 +    else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule then
    8.19        line :: lines
    8.20      else if role = Axiom then
    8.21        lines (* axioms (facts) need no proof lines *)