src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
changeset 50047 45684acf0b94
parent 49981 e12b4e9794fd
child 50048 fb024bbf4b65
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sun Nov 11 19:56:02 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Nov 12 11:32:22 2012 +0100
     1.3 @@ -23,7 +23,7 @@
     1.4    val fact_from_ref :
     1.5      Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
     1.6      -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
     1.7 -  val backquote_thm : thm -> string
     1.8 +  val backquote_thm : Proof.context -> thm -> string
     1.9    val clasimpset_rule_table_of : Proof.context -> status Termtab.table
    1.10    val maybe_instantiate_inducts :
    1.11      Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
    1.12 @@ -231,10 +231,10 @@
    1.13      exists_low_level_class_const t orelse is_that_fact th
    1.14    end
    1.15  
    1.16 -fun hackish_string_for_term thy t =
    1.17 +fun hackish_string_for_term ctxt t =
    1.18    Print_Mode.setmp
    1.19      (filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ()))
    1.20 -    (Syntax.string_of_term_global thy) t
    1.21 +    (Syntax.string_of_term ctxt) t
    1.22    |> String.translate (fn c => if Char.isPrint c then str c else "")
    1.23    |> simplify_spaces
    1.24  
    1.25 @@ -259,12 +259,12 @@
    1.26            (Term.add_vars t [] |> sort_wrt (fst o fst))
    1.27    |> fst
    1.28  
    1.29 -fun backquote_term thy t =
    1.30 +fun backquote_term ctxt t =
    1.31    t |> close_form
    1.32 -    |> hackish_string_for_term thy
    1.33 +    |> hackish_string_for_term ctxt
    1.34      |> backquote
    1.35  
    1.36 -fun backquote_thm th = backquote_term (theory_of_thm th) (prop_of th)
    1.37 +fun backquote_thm ctxt th = backquote_term ctxt (prop_of th)
    1.38  
    1.39  fun clasimpset_rule_table_of ctxt =
    1.40    let
    1.41 @@ -328,14 +328,13 @@
    1.42  
    1.43  fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x =
    1.44    let
    1.45 -    val thy = Proof_Context.theory_of ctxt
    1.46      fun varify_noninducts (t as Free (s, T)) =
    1.47          if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
    1.48        | varify_noninducts t = t
    1.49      val p_inst =
    1.50        concl_prop |> map_aterms varify_noninducts |> close_form
    1.51                   |> lambda (Free ind_x)
    1.52 -                 |> hackish_string_for_term thy
    1.53 +                 |> hackish_string_for_term ctxt
    1.54    in
    1.55      ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
    1.56        stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)])
    1.57 @@ -417,7 +416,7 @@
    1.58                               val new =
    1.59                                 (((fn () =>
    1.60                                       if name0 = "" then
    1.61 -                                       backquote_thm th
    1.62 +                                       backquote_thm ctxt th
    1.63                                       else
    1.64                                         [Facts.extern ctxt facts name0,
    1.65                                          Name_Space.extern ctxt full_space name0]