src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
changeset 51998 f732a674db1b
parent 51160 599ff65b85e2
child 52031 9a9238342963
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed May 15 17:27:24 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed May 15 17:43:42 2013 +0200
     1.3 @@ -245,7 +245,7 @@
     1.4    (not (Config.get ctxt ignore_no_atp) andalso is_package_def name) orelse
     1.5    exists (fn s => String.isSuffix s name) (multi_base_blacklist ctxt ho_atp)
     1.6  
     1.7 -fun hackish_string_for_term ctxt =
     1.8 +fun hackish_string_of_term ctxt =
     1.9    with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces
    1.10  
    1.11  (* This is a terrible hack. Free variables are sometimes coded as "M__" when
    1.12 @@ -269,12 +269,8 @@
    1.13            (Term.add_vars t [] |> sort_wrt (fst o fst))
    1.14    |> fst
    1.15  
    1.16 -fun backquote_term ctxt t =
    1.17 -  t |> close_form
    1.18 -    |> hackish_string_for_term ctxt
    1.19 -    |> backquote
    1.20 -
    1.21 -fun backquote_thm ctxt th = backquote_term ctxt (prop_of th)
    1.22 +fun backquote_term ctxt = close_form #> hackish_string_of_term ctxt #> backquote
    1.23 +fun backquote_thm ctxt = backquote_term ctxt o prop_of
    1.24  
    1.25  fun clasimpset_rule_table_of ctxt =
    1.26    let
    1.27 @@ -384,7 +380,7 @@
    1.28      val p_inst =
    1.29        concl_prop |> map_aterms varify_noninducts |> close_form
    1.30                   |> lambda (Free ind_x)
    1.31 -                 |> hackish_string_for_term ctxt
    1.32 +                 |> hackish_string_of_term ctxt
    1.33    in
    1.34      ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
    1.35        stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)])