1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Sep 03 15:24:39 2019 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Sep 03 16:10:31 2019 +0200
     1.3 @@ -45,7 +45,7 @@
     1.4  
     1.5  open String_Redirect
     1.6  
     1.7 -val trace = Attrib.setup_config_bool @{binding sledgehammer_isar_trace} (K false)
     1.8 +val trace = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_isar_trace\<close> (K false)
     1.9  
    1.10  val e_definition_rule = "definition"
    1.11  val e_skolemize_rule = "skolemize"
    1.12 @@ -55,7 +55,6 @@
    1.13  val vampire_skolemisation_rule = "skolemisation"
    1.14  val veriT_la_generic_rule = "la_generic"
    1.15  val veriT_simp_arith_rule = "simp_arith"
    1.16 -val veriT_tmp_ite_elim_rule = "tmp_ite_elim"
    1.17  val veriT_tmp_skolemize_rule = "tmp_skolemize"
    1.18  val z3_skolemize_rule = Z3_Proof.string_of_rule Z3_Proof.Skolemize
    1.19  val z3_th_lemma_rule_prefix = Z3_Proof.string_of_rule (Z3_Proof.Th_Lemma "")
    1.20 @@ -63,7 +62,7 @@
    1.21  
    1.22  val skolemize_rules =
    1.23    [e_definition_rule, e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule,
    1.24 -   spass_skolemize_rule, vampire_skolemisation_rule, veriT_tmp_ite_elim_rule,
    1.25 +   spass_skolemize_rule, vampire_skolemisation_rule,
    1.26     veriT_tmp_skolemize_rule, waldmeister_skolemize_rule, z3_skolemize_rule, zipperposition_cnf_rule]
    1.27  
    1.28  fun is_ext_rule rule = (rule = leo2_extcnf_equal_neg_rule)
    1.29 @@ -90,7 +89,7 @@
    1.30         definitions. *)
    1.31      if role = Conjecture orelse role = Negated_Conjecture then
    1.32        line :: lines
    1.33 -    else if t aconv @{prop True} then
    1.34 +    else if t aconv \<^prop>\<open>True\<close> then
    1.35        map (replace_dependencies_in_line (name, [])) lines
    1.36      else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule then
    1.37        line :: lines
    1.38 @@ -114,7 +113,7 @@
    1.39               Term.aconv_untyped (normalize prev_role prev_t, norm_t)))
    1.40            res
    1.41  
    1.42 -      fun looks_boring () = t aconv @{prop False} orelse length deps < 2
    1.43 +      fun looks_boring () = t aconv \<^prop>\<open>False\<close> orelse length deps < 2
    1.44  
    1.45        fun is_skolemizing_line (_, _, _, rule', deps') =
    1.46          is_skolemize_rule rule' andalso member (op =) deps' name
    1.47 @@ -281,7 +280,7 @@
    1.48                      (negs as _ :: _, pos as _ :: _) =>
    1.49                      s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs),
    1.50                        Library.foldr1 s_disj pos)
    1.51 -                  | _ => fold (curry s_disj) lits @{term False})
    1.52 +                  | _ => fold (curry s_disj) lits \<^term>\<open>False\<close>)
    1.53                  end
    1.54                  |> HOLogic.mk_Trueprop |> finish_off
    1.55