# HG changeset patch
# User haftmann
# Date 1277406212 -7200
# Node ID f5a4b7ac635f174f842cd66d8dbcbba49c67d163
# Parent  2e733b0a963ce59478294fb740ce07dfd61433ff# Parent  456dd03e8ccef13a9d7ff9a091b03ae7901b39ba
merged

diff -r 456dd03e8cce -r f5a4b7ac635f Admin/CHECKLIST
--- a/Admin/CHECKLIST	Thu Jun 24 18:45:31 2010 +0200
+++ b/Admin/CHECKLIST	Thu Jun 24 21:03:32 2010 +0200
@@ -29,3 +29,17 @@
     build
     lib/html/library_index_content.template
 
+
+Packaging
+=========
+
+- makedist -r DISTNAME
+
+- makebin (multiplatform);
+
+- makebin -l on fast machine;
+
+- makebundle (multiplatform);
+
+- hdiutil create -srcfolder DIR DMG (Mac OS);
+
diff -r 456dd03e8cce -r f5a4b7ac635f src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Jun 24 18:45:31 2010 +0200
+++ b/src/HOL/IsaMakefile	Thu Jun 24 21:03:32 2010 +0200
@@ -1093,6 +1093,7 @@
 
 $(OUT)/HOL-Multivariate_Analysis: $(OUT)/HOL				\
   Multivariate_Analysis/Brouwer_Fixpoint.thy				\
+  Multivariate_Analysis/Cartesian_Euclidean_Space.thy                   \
   Multivariate_Analysis/Convex_Euclidean_Space.thy			\
   Multivariate_Analysis/Derivative.thy					\
   Multivariate_Analysis/Determinants.thy				\
diff -r 456dd03e8cce -r f5a4b7ac635f src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Thu Jun 24 18:45:31 2010 +0200
+++ b/src/HOL/Sledgehammer.thy	Thu Jun 24 21:03:32 2010 +0200
@@ -53,16 +53,6 @@
 lemma equal_imp_fequal [no_atp]: "X = Y \<Longrightarrow> fequal X Y"
   by (simp add: fequal_def)
 
-text{*These two represent the equivalence between Boolean equality and iff.
-They can't be converted to clauses automatically, as the iff would be
-expanded...*}
-
-lemma iff_positive: "P \<or> Q \<or> P = Q"
-by blast
-
-lemma iff_negative: "\<not> P \<or> \<not> Q \<or> P = Q"
-by blast
-
 text{*Theorems for translation to combinators*}
 
 lemma abs_S [no_atp]: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"
diff -r 456dd03e8cce -r f5a4b7ac635f src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Thu Jun 24 18:45:31 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Thu Jun 24 21:03:32 2010 +0200
@@ -7,13 +7,13 @@
 signature QUOTIENT_DEF =
 sig
   val quotient_def: (binding option * mixfix) * (Attrib.binding * (term * term)) ->
-    local_theory -> (term * thm) * local_theory
+    local_theory -> Quotient_Info.qconsts_info * local_theory
 
   val quotdef_cmd: (binding option * mixfix) * (Attrib.binding * (string * string)) ->
-    local_theory -> (term * thm) * local_theory
+    local_theory -> Quotient_Info.qconsts_info * local_theory
 
-  val quotient_lift_const: typ list -> string * term -> local_theory ->
-    (term * thm) * local_theory
+  val lift_raw_const: typ list -> string * term -> local_theory ->
+    Quotient_Info.qconsts_info * local_theory
 end;
 
 structure Quotient_Def: QUOTIENT_DEF =
@@ -32,12 +32,10 @@
     - the new constant as term
     - the rhs of the definition as term
 
-   It returns the defined constant and its definition
-   theorem; stores the data in the qconsts data slot.
+   It stores the qconst_info in the qconsts data slot.
 
-   Restriction: At the moment the right-hand side of the
-   definition must be a constant. Similarly the left-hand 
-   side must be a constant.
+   Restriction: At the moment the left- and right-hand 
+   side of the definition must be a constant. 
 *)
 fun error_msg bind str = 
 let 
@@ -45,7 +43,7 @@
   val pos = Position.str_of (Binding.pos_of bind)
 in
   error ("Head of quotient_definition " ^ 
-    (quote str) ^ " differs from declaration " ^ name ^ pos)
+    quote str ^ " differs from declaration " ^ name ^ pos)
 end
 
 fun quotient_def ((optbind, mx), (attr, (lhs, rhs))) lthy =
@@ -69,12 +67,14 @@
   val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy
 
   (* data storage *)
-  fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm}
+  val qconst_data = {qconst = trm, rconst = rhs, def = thm}
+
+  fun qcinfo phi = transform_qconsts phi qconst_data
   fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)
   val lthy'' = Local_Theory.declaration true
                  (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'
 in
-  ((trm, thm), lthy'')
+  (qconst_data, lthy'')
 end
 
 fun quotdef_cmd (decl, (attr, (lhs_str, rhs_str))) lthy =
@@ -87,10 +87,17 @@
   quotient_def (decl, (attr, (lhs, rhs))) lthy''
 end
 
-fun quotient_lift_const qtys (b, t) ctxt =
+(* a wrapper for automatically lifting a raw constant *)
+fun lift_raw_const qtys (qconst_name, rconst) ctxt =
+let
+  val rty = fastype_of rconst
+  val qty = derive_qtyp qtys rty ctxt
+in
   quotient_def ((NONE, NoSyn), (Attrib.empty_binding,
-    (Quotient_Term.quotient_lift_const qtys (b, t) ctxt, t))) ctxt
+    (Free (qconst_name, qty), rconst))) ctxt
+end
 
+(* parser and command *)
 val quotdef_decl = (Parse.binding >> SOME) -- Parse.opt_mixfix' --| Parse.$$$ "where"
 
 val quotdef_parser =
diff -r 456dd03e8cce -r f5a4b7ac635f src/HOL/Tools/Quotient/quotient_term.ML
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Thu Jun 24 18:45:31 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Thu Jun 24 21:03:32 2010 +0200
@@ -26,7 +26,7 @@
   val inj_repabs_trm: Proof.context -> term * term -> term
   val inj_repabs_trm_chk: Proof.context -> term * term -> term
 
-  val quotient_lift_const: typ list -> string * term -> local_theory -> term
+  val derive_qtyp: typ list -> typ -> Proof.context -> typ
   val quotient_lift_all: typ list -> Proof.context -> term -> term
 end;
 
@@ -84,7 +84,7 @@
 *)
 fun mk_mapfun ctxt vs rty =
 let
-  val vs' = map (mk_Free) vs
+  val vs' = map mk_Free vs
 
   fun mk_mapfun_aux rty =
     case rty of
@@ -103,7 +103,7 @@
 let
   val thy = ProofContext.theory_of ctxt
   val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
-  val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
+  val qdata = quotdata_lookup thy s handle Quotient_Info.NotFound => raise exn
 in
   (#rtyp qdata, #qtyp qdata)
 end
@@ -738,14 +738,12 @@
   (ty_substs, filter valid_trm_subst all_trm_substs)
 end
 
-fun quotient_lift_const qtys (b, t) ctxt =
+fun derive_qtyp qtys rty ctxt =
 let
   val thy = ProofContext.theory_of ctxt
-  val (ty_substs, _) = get_ty_trm_substs qtys ctxt;
-  val (_, ty) = dest_Const t;
-  val nty = subst_tys thy ty_substs ty;
+  val (ty_substs, _) = get_ty_trm_substs qtys ctxt
 in
-  Free(b, nty)
+  subst_tys thy ty_substs rty
 end
 
 (*
diff -r 456dd03e8cce -r f5a4b7ac635f src/HOL/Tools/Quotient/quotient_typ.ML
--- a/src/HOL/Tools/Quotient/quotient_typ.ML	Thu Jun 24 18:45:31 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Thu Jun 24 21:03:32 2010 +0200
@@ -8,7 +8,7 @@
 signature QUOTIENT_TYPE =
 sig
   val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool)) * thm
-    -> Proof.context -> (thm * thm) * local_theory
+    -> Proof.context -> Quotient_Info.quotdata_info * local_theory
 
   val quotient_type: ((string list * binding * mixfix) * (typ * term * bool)) list
     -> Proof.context -> Proof.state
@@ -32,11 +32,8 @@
 end
 
 fun note (name, thm, attrs) lthy =
-let
-  val ((_,[thm']), lthy') = Local_Theory.note ((name, attrs), [thm]) lthy
-in
-  (thm', lthy')
-end
+  Local_Theory.note ((name, attrs), [thm]) lthy |> snd
+
 
 fun intern_attr at = Attrib.internal (K at)
 
@@ -64,7 +61,7 @@
     |> map Free
 in
   lambda c (HOLogic.exists_const rty $
-     lambda x (HOLogic.mk_conj ((rel $ x $ x), (HOLogic.mk_eq (c, (rel $ x))))))
+     lambda x (HOLogic.mk_conj (rel $ x $ x, HOLogic.mk_eq (c, rel $ x))))
 end
 
 
@@ -139,7 +136,10 @@
 (* main function for constructing a quotient type *)
 fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial)), equiv_thm) lthy =
 let
-  val part_equiv = if partial then equiv_thm else equiv_thm RS @{thm equivp_implies_part_equivp}
+  val part_equiv = 
+    if partial 
+    then equiv_thm 
+    else equiv_thm RS @{thm equivp_implies_part_equivp}
 
   (* generates the typedef *)
   val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy
@@ -173,15 +173,17 @@
   (* name equivalence theorem *)
   val equiv_thm_name = Binding.suffix_name "_equivp" qty_name
 
-  (* storing the quot-info *)
-  fun qinfo phi = transform_quotdata phi
-    {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
-  val lthy4 = Local_Theory.declaration true
-    (fn phi => quotdata_update_gen qty_full_name (qinfo phi)) lthy3
+  (* storing the quotdata *)
+  val quotdata = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
+
+  fun qinfo phi = transform_quotdata phi quotdata
+
+  val lthy4 = lthy3
+     |> Local_Theory.declaration true (fn phi => quotdata_update_gen qty_full_name (qinfo phi))
+     |> note (equiv_thm_name, equiv_thm, if partial then [] else [intern_attr equiv_rules_add])
+     |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add])
 in
-  lthy4
-  |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add])
-  ||>> note (equiv_thm_name, equiv_thm, if partial then [] else [intern_attr equiv_rules_add])
+  (quotdata, lthy4)
 end
 
 
@@ -253,6 +255,7 @@
  - its free type variables (first argument)
  - its mixfix annotation
  - the type to be quotient
+ - the partial flag (a boolean)
  - the relation according to which the type is quotient
 
  it opens a proof-state in which one has to show that the
@@ -268,7 +271,8 @@
   fun mk_goal (rty, rel, partial) =
   let
     val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
-    val const = if partial then @{const_name part_equivp} else @{const_name equivp}
+    val const = 
+      if partial then @{const_name part_equivp} else @{const_name equivp}
   in
     HOLogic.mk_Trueprop (Const (const, equivp_ty) $ rel)
   end
diff -r 456dd03e8cce -r f5a4b7ac635f src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Jun 24 18:45:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Jun 24 21:03:32 2010 +0200
@@ -679,8 +679,7 @@
       (*The modes FO and FT are sticky. HO can be downgraded to FO.*)
       fun set_mode FO = FO
         | set_mode HO =
-          if forall (is_quasi_fol_term thy o prop_of) (cls @ ths) then FO
-          else HO
+          if forall (is_quasi_fol_theorem thy) (cls @ ths) then FO else HO
         | set_mode FT = FT
       val mode = set_mode mode0
       (*transform isabelle clause to metis clause *)
diff -r 456dd03e8cce -r f5a4b7ac635f src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Jun 24 18:45:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Jun 24 21:03:32 2010 +0200
@@ -21,7 +21,7 @@
   val tvar_classes_of_terms : term list -> string list
   val tfree_classes_of_terms : term list -> string list
   val type_consts_of_terms : theory -> term list -> string list
-  val is_quasi_fol_term : theory -> term -> bool
+  val is_quasi_fol_theorem : theory -> thm -> bool
   val relevant_facts :
     bool -> bool -> real -> real -> bool -> int -> bool -> relevance_override
     -> Proof.context * (thm list * 'a) -> thm list -> cnf_thm list
@@ -88,42 +88,70 @@
   Symtab.map_default (c, [ctyps])
                      (fn [] => [] | ctypss => insert (op =) ctyps ctypss)
 
-val fresh_Ex_prefix = "Sledgehammer.Ex."
+val fresh_sko_prefix = "Sledgehammer.Skox."
+
+val flip = Option.map not
 
-fun get_goal_consts_typs thy goals =
+(* Including equality in this list might be expected to stop rules like
+   subset_antisym from being chosen, but for some reason filtering works better
+   with them listed. The logical signs All, Ex, &, and --> are omitted for CNF
+   because any remaining occurrences must be within comprehensions. *)
+val boring_cnf_consts =
+  [@{const_name Trueprop}, @{const_name "==>"}, @{const_name all},
+   @{const_name "=="}, @{const_name "op |"}, @{const_name Not},
+   @{const_name "op ="}]
+
+fun get_consts_typs thy pos ts =
   let
-    val use_natural_form = !use_natural_form
     (* Free variables are included, as well as constants, to handle locales.
        "skolem_id" is included to increase the complexity of theorems containing
        Skolem functions. In non-CNF form, "Ex" is included but each occurrence
        is considered fresh, to simulate the effect of Skolemization. *)
-    fun aux (Const (x as (s, _))) =
-        (if s = @{const_name Ex} andalso use_natural_form then
-           (gensym fresh_Ex_prefix, [])
-         else
-           (const_with_typ thy x))
-        |> add_const_type_to_table
-      | aux (Free x) = add_const_type_to_table (const_with_typ thy x)
-      | aux ((t as Const (@{const_name skolem_id}, _)) $ _) = aux t
-      | aux (t $ u) = aux t #> aux u
-      | aux (Abs (_, _, t)) = aux t
-      | aux _ = I
-    (* Including equality in this list might be expected to stop rules like
-       subset_antisym from being chosen, but for some reason filtering works better
-       with them listed. The logical signs All, Ex, &, and --> are omitted for CNF
-       because any remaining occurrences must be within comprehensions. *)
-    val standard_consts =
-      [@{const_name Trueprop}, @{const_name "==>"}, @{const_name all},
-       @{const_name "=="}, @{const_name "op |"}, @{const_name Not},
-       @{const_name "op ="}] @
-      (if use_natural_form then
-         [@{const_name All}, @{const_name Ex}, @{const_name "op &"},
-          @{const_name "op -->"}]
-       else
-         [])
+    fun do_term t =
+      case t of
+        Const x => add_const_type_to_table (const_with_typ thy x)
+      | Free x => add_const_type_to_table (const_with_typ thy x)
+      | (t as Const (@{const_name skolem_id}, _)) $ _ => do_term t
+      | t1 $ t2 => do_term t1 #> do_term t2
+      | Abs (_, _, t) => do_term t
+      | _ => I
+    fun do_quantifier sweet_pos pos body_t =
+      do_formula pos body_t
+      #> (if pos = SOME sweet_pos then I
+          else add_const_type_to_table (gensym fresh_sko_prefix, []))
+    and do_equality T t1 t2 =
+      fold (if T = @{typ bool} orelse T = @{typ prop} then do_formula NONE
+            else do_term) [t1, t2]
+    and do_formula pos t =
+      case t of
+        Const (@{const_name all}, _) $ Abs (_, _, body_t) =>
+        do_quantifier false pos body_t
+      | @{const "==>"} $ t1 $ t2 =>
+        do_formula (flip pos) t1 #> do_formula pos t2
+      | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
+        do_equality T t1 t2
+      | @{const Trueprop} $ t1 => do_formula pos t1
+      | @{const Not} $ t1 => do_formula (flip pos) t1
+      | Const (@{const_name All}, _) $ Abs (_, _, body_t) =>
+        do_quantifier false pos body_t
+      | Const (@{const_name Ex}, _) $ Abs (_, _, body_t) =>
+        do_quantifier true pos body_t
+      | @{const "op &"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
+      | @{const "op |"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
+      | @{const "op -->"} $ t1 $ t2 =>
+        do_formula (flip pos) t1 #> do_formula pos t2
+      | Const (@{const_name "op ="}, Type (_, [T, _])) $ t1 $ t2 =>
+        do_equality T t1 t2
+      | (t0 as Const (_, @{typ bool})) $ t1 =>
+        do_term t0 #> do_formula pos t1  (* theory constant *)
+      | _ => do_term t
   in
-    Symtab.empty |> fold (Symtab.update o rpair []) standard_consts
-                 |> fold aux goals
+    Symtab.empty
+    |> (if !use_natural_form then
+          fold (do_formula pos) ts
+        else
+          fold (Symtab.update o rpair []) boring_cnf_consts
+          #> fold do_term ts)
   end
 
 (*Inserts a dummy "constant" referring to the theory name, so that relevance
@@ -217,7 +245,7 @@
 fun add_expand_pairs (x,ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys;
 
 fun consts_typs_of_term thy t =
-  Symtab.fold add_expand_pairs (get_goal_consts_typs thy [t]) []
+  Symtab.fold add_expand_pairs (get_consts_typs thy (SOME false) [t]) []
 
 fun pair_consts_typs_axiom theory_relevant thy axiom =
   (axiom, axiom |> appropriate_prop_of theory_relevant
@@ -306,9 +334,11 @@
               if weight >= threshold orelse
                  (defs_relevant andalso
                   defines thy (#1 clsthm) rel_const_tab) then
-                (trace_msg (fn () => name ^ " clause " ^ Int.toString n ^
-                                     " passes: " ^ Real.toString weight);
-                relevant ((ax, weight) :: newrels, rejects) axs)
+                (trace_msg (fn () =>
+                     name ^ " clause " ^ Int.toString n ^
+                     " passes: " ^ Real.toString weight
+                     (* ^ " consts: " ^ commas (map fst consts_typs) *));
+                 relevant ((ax, weight) :: newrels, rejects) axs)
               else
                 relevant (newrels, ax :: rejects) axs
             end
@@ -322,11 +352,15 @@
 fun relevance_filter ctxt relevance_threshold relevance_convergence
                      defs_relevant max_new theory_relevant relevance_override
                      thy (axioms : cnf_thm list) goals =
-  if relevance_threshold > 0.0 then
+  if relevance_threshold > 1.0 then
+    []
+  else if relevance_threshold < 0.0 then
+    axioms
+  else
     let
       val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
                            Symtab.empty
-      val goal_const_tab = get_goal_consts_typs thy goals
+      val goal_const_tab = get_consts_typs thy (SOME true) goals
       val _ =
         trace_msg (fn () => "Initial constants: " ^
                             commas (Symtab.keys goal_const_tab))
@@ -340,8 +374,6 @@
       trace_msg (fn () => "Total relevant: " ^ Int.toString (length relevant));
       relevant
     end
-  else
-    axioms;
 
 (***************************************************************)
 (* Retrieving and filtering lemmas                             *)
@@ -374,6 +406,9 @@
 fun subtract_cls ax_clauses =
   filter_out (Termtab.defined (mk_clause_table ax_clauses) o prop_of)
 
+val exists_sledgehammer_const =
+  exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s) o prop_of
+
 fun all_name_thms_pairs respect_no_atp ctxt chained_ths =
   let
     val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
@@ -396,7 +431,8 @@
 
             val name1 = Facts.extern facts name;
             val name2 = Name_Space.extern full_space name;
-            val ths = filter_out is_theorem_bad_for_atps ths0;
+            val ths = filter_out (is_theorem_bad_for_atps orf
+                                  exists_sledgehammer_const) ths0
           in
             case find_first check_thms [name1, name2, name] of
               NONE => I
@@ -483,13 +519,8 @@
 (* ATP invocation methods setup                                *)
 (***************************************************************)
 
-fun is_quasi_fol_term thy =
-  Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 []
-
-(*Ensures that no higher-order theorems "leak out"*)
-fun restrict_to_logic thy true cls =
-    filter (is_quasi_fol_term thy o prop_of o fst) cls
-  | restrict_to_logic _ false cls = cls
+fun is_quasi_fol_theorem thy =
+  Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 [] o prop_of
 
 (**** Predicates to detect unwanted clauses (prolific or likely to cause
       unsoundness) ****)
@@ -539,43 +570,35 @@
     (has_typed_var dangerous_types t orelse
      forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t)))
 
-fun remove_dangerous_clauses full_types add_thms =
-  filter_out (fn (cnf_th, (_, orig_th)) =>
-                 not (member Thm.eq_thm add_thms orig_th) andalso
-                 is_dangerous_term full_types (prop_of cnf_th))
-
 fun is_fol_goal thy = forall (Meson.is_fol_term thy) o map prop_of
 
 fun relevant_facts full_types respect_no_atp relevance_threshold
                    relevance_convergence defs_relevant max_new theory_relevant
                    (relevance_override as {add, del, only})
                    (ctxt, (chained_ths, _)) goal_cls =
-  if (only andalso null add) orelse relevance_threshold > 1.0 then
-    []
-  else
-    let
-      val thy = ProofContext.theory_of ctxt
-      val has_override = not (null add) orelse not (null del)
-      val is_FO = is_fol_goal thy goal_cls
-      val axioms =
-        checked_name_thm_pairs (respect_no_atp andalso not only) ctxt
-            (if only then map (name_thms_pair_from_ref ctxt chained_ths) add
-             else all_name_thms_pairs respect_no_atp ctxt chained_ths)
-        |> cnf_rules_pairs thy
-        |> not has_override ? make_unique
-        |> not only ? restrict_to_logic thy is_FO
-        |> (if only then
-              I
-            else
-              remove_dangerous_clauses full_types
-                                       (maps (ProofContext.get_fact ctxt) add))
-    in
-      relevance_filter ctxt relevance_threshold relevance_convergence
-                       defs_relevant max_new theory_relevant relevance_override
-                       thy axioms (map prop_of goal_cls)
-      |> has_override ? make_unique
-      |> sort (prod_ord string_ord int_ord o pairself (fst o snd))
-    end
+  let
+    val thy = ProofContext.theory_of ctxt
+    val add_thms = maps (ProofContext.get_fact ctxt) add
+    val has_override = not (null add) orelse not (null del)
+    val is_FO = is_fol_goal thy goal_cls
+    val axioms =
+      checked_name_thm_pairs (respect_no_atp andalso not only) ctxt
+          (map (name_thms_pair_from_ref ctxt chained_ths) add @
+           (if only then []
+            else all_name_thms_pairs respect_no_atp ctxt chained_ths))
+      |> cnf_rules_pairs thy
+      |> not has_override ? make_unique
+      |> filter (fn (cnf_thm, (_, orig_thm)) =>
+                    member Thm.eq_thm add_thms orig_thm orelse
+                    ((not is_FO orelse is_quasi_fol_theorem thy cnf_thm) andalso
+                     not (is_dangerous_term full_types (prop_of cnf_thm))))
+  in
+    relevance_filter ctxt relevance_threshold relevance_convergence
+                     defs_relevant max_new theory_relevant relevance_override
+                     thy axioms (map prop_of goal_cls)
+    |> has_override ? make_unique
+    |> sort (prod_ord string_ord int_ord o pairself (fst o snd))
+  end
 
 (** Helper clauses **)
 
diff -r 456dd03e8cce -r f5a4b7ac635f src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Thu Jun 24 18:45:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Thu Jun 24 21:03:32 2010 +0200
@@ -8,6 +8,8 @@
 signature SLEDGEHAMMER_FACT_PREPROCESSOR =
 sig
   type cnf_thm = thm * ((string * int) * thm)
+
+  val sledgehammer_prefix: string
   val chained_prefix: string
   val trace: bool Unsynchronized.ref
   val trace_msg: (unit -> string) -> unit
@@ -35,13 +37,15 @@
 
 type cnf_thm = thm * ((string * int) * thm)
 
+val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
+
 (* Used to label theorems chained into the goal. *)
-val chained_prefix = "Sledgehammer.chained_"
+val chained_prefix = sledgehammer_prefix ^ "chained_"
 
 val trace = Unsynchronized.ref false;
 fun trace_msg msg = if !trace then tracing (msg ()) else ();
 
-val skolem_theory_name = "Sledgehammer.Sko"
+val skolem_theory_name = sledgehammer_prefix ^ "Sko"
 val skolem_prefix = "sko_"
 val skolem_infix = "$"
 
@@ -183,25 +187,14 @@
 fun vars_of_thm th =
   map (Thm.cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []);
 
-(*Make a version of fun_cong with a given variable name*)
-local
-    val fun_cong' = fun_cong RS asm_rl; (*renumber f, g to prevent clashes with (a,0)*)
-    val cx = hd (vars_of_thm fun_cong');
-    val ty = typ_of (ctyp_of_term cx);
-    val thy = theory_of_thm fun_cong;
-    fun mkvar a = cterm_of thy (Var((a,0),ty));
-in
-fun xfun_cong x = Thm.instantiate ([], [(cx, mkvar x)]) fun_cong'
-end;
+val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]}
 
-(*Removes the lambdas from an equation of the form t = (%x. u).  A non-negative n,
-  serves as an upper bound on how many to remove.*)
-fun strip_lambdas 0 th = th
-  | strip_lambdas n th =
-      case prop_of th of
-          _ $ (Const (@{const_name "op ="}, _) $ _ $ Abs (x, _, _)) =>
-              strip_lambdas (n-1) (freeze_thm (th RS xfun_cong x))
-        | _ => th;
+(* Removes the lambdas from an equation of the form t = (%x. u). *)
+fun extensionalize th =
+  case prop_of th of
+    _ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _]))
+         $ _ $ Abs (s, _, _)) => extensionalize (th RS fun_cong_all)
+  | _ => th
 
 fun is_quasi_lambda_free (Const (@{const_name skolem_id}, _) $ _) = true
   | is_quasi_lambda_free (t1 $ t2) =
@@ -339,9 +332,9 @@
 fun to_nnf th ctxt0 =
   let val th1 = th |> transform_elim |> zero_var_indexes
       val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
-      val th3 = th2
-        |> Conv.fconv_rule Object_Logic.atomize
-        |> Meson.make_nnf ctxt |> strip_lambdas ~1
+      val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize
+                    |> extensionalize
+                    |> Meson.make_nnf ctxt
   in  (th3, ctxt)  end;
 
 (*Generate Skolem functions for a theorem supplied in nnf*)
diff -r 456dd03e8cce -r f5a4b7ac635f src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Thu Jun 24 18:45:31 2010 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Thu Jun 24 21:03:32 2010 +0200
@@ -334,10 +334,10 @@
   in
     Pretty.block
      ([str "(fn ", mk_tuple out_ps, str " =>", Pretty.brk 1] @
-      (Pretty.block ((if eqs=[] then [] else str "if " ::
+      (Pretty.block ((if null eqs then [] else str "if " ::
          [Pretty.block eqs, Pretty.brk 1, str "then "]) @
          (success_p ::
-          (if eqs=[] then [] else [Pretty.brk 1, str "else DSeq.empty"]))) ::
+          (if null eqs then [] else [Pretty.brk 1, str "else DSeq.empty"]))) ::
        (if can_fail then
           [Pretty.brk 1, str "| _ => DSeq.empty)"]
         else [str ")"])))
diff -r 456dd03e8cce -r f5a4b7ac635f src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Thu Jun 24 18:45:31 2010 +0200
+++ b/src/HOL/Tools/meson.ML	Thu Jun 24 21:03:32 2010 +0200
@@ -521,10 +521,9 @@
   nnf_ss also includes the one-point simprocs,
   which are needed to avoid the various one-point theorems from generating junk clauses.*)
 val nnf_simps =
-  [@{thm simp_implies_def}, @{thm Ex1_def}, @{thm Ball_def},@{thm  Bex_def}, @{thm if_True},
-    @{thm if_False}, @{thm if_cancel}, @{thm if_eq_cancel}, @{thm cases_simp}];
-val nnf_extra_simps =
-  @{thms split_ifs} @ @{thms ex_simps} @ @{thms all_simps} @ @{thms simp_thms};
+  @{thms simp_implies_def Ex1_def Ball_def Bex_def if_True if_False if_cancel
+         if_eq_cancel cases_simp}
+val nnf_extra_simps = @{thms split_ifs ex_simps all_simps simp_thms}
 
 val nnf_ss =
   HOL_basic_ss addsimps nnf_extra_simps
diff -r 456dd03e8cce -r f5a4b7ac635f src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Thu Jun 24 18:45:31 2010 +0200
+++ b/src/Pure/General/pretty.ML	Thu Jun 24 21:03:32 2010 +0200
@@ -102,10 +102,11 @@
 
 (** printing items: compound phrases, strings, and breaks **)
 
-datatype T =
+abstype T =
   Block of (output * output) * T list * int * int |  (*markup output, body, indentation, length*)
   String of output * int |                           (*text, length*)
-  Break of bool * int;                               (*mandatory flag, width if not taken*)
+  Break of bool * int                                (*mandatory flag, width if not taken*)
+with
 
 fun length (Block (_, _, _, len)) = len
   | length (String (_, len)) = len
@@ -323,6 +324,8 @@
   | from_ML (ML_Pretty.String s) = String s
   | from_ML (ML_Pretty.Break b) = Break b;
 
+end;
+
 
 
 (** abstract pretty printing context **)
diff -r 456dd03e8cce -r f5a4b7ac635f src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Thu Jun 24 18:45:31 2010 +0200
+++ b/src/Pure/Isar/code.ML	Thu Jun 24 21:03:32 2010 +0200
@@ -1132,7 +1132,7 @@
     fun mk_prem z = Free (z, T_cong);
     fun mk_concl z = list_comb (Const (case_const, T), map2 (curry Free) (ws @ z :: vs) Ts);
     val (prem, concl) = pairself Logic.mk_equals (pairself mk_prem (x, y), pairself mk_concl (x, y));
-    fun tac { prems, ... } = Simplifier.rewrite_goals_tac prems
+    fun tac { context, prems } = Simplifier.rewrite_goals_tac prems
       THEN ALLGOALS (ProofContext.fact_tac [Drule.reflexive_thm]);
   in Skip_Proof.prove_global thy (x :: y :: zs) [prem] concl tac end;
 
diff -r 456dd03e8cce -r f5a4b7ac635f src/Pure/net.ML
--- a/src/Pure/net.ML	Thu Jun 24 18:45:31 2010 +0200
+++ b/src/Pure/net.ML	Thu Jun 24 21:03:32 2010 +0200
@@ -17,6 +17,7 @@
 sig
   type key
   val key_of_term: term -> key list
+  val encode_type: typ -> term
   type 'a net
   val empty: 'a net
   exception INSERT
@@ -62,6 +63,11 @@
 (*convert a term to a list of keys*)
 fun key_of_term t = add_key_of_terms (t, []);
 
+(*encode_type -- for indexing purposes*)
+fun encode_type (Type (c, Ts)) = Term.list_comb (Const (c, dummyT), map encode_type Ts)
+  | encode_type (TFree (a, _)) = Free (a, dummyT)
+  | encode_type (TVar (a, _)) = Var (a, dummyT);
+
 
 (*Trees indexed by key lists: each arc is labelled by a key.
   Each node contains a list of items, and arcs to children.
diff -r 456dd03e8cce -r f5a4b7ac635f src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Thu Jun 24 18:45:31 2010 +0200
+++ b/src/Pure/pure_setup.ML	Thu Jun 24 21:03:32 2010 +0200
@@ -18,6 +18,7 @@
 
 (* ML toplevel pretty printing *)
 
+toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
 toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
 toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
 toplevel_pp ["Position", "T"] "Pretty.position";
diff -r 456dd03e8cce -r f5a4b7ac635f src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Thu Jun 24 18:45:31 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Thu Jun 24 21:03:32 2010 +0200
@@ -142,9 +142,9 @@
       name_syntax_table = name_syntax_table2, module_alias = module_alias2 }) =
   if serial1 = serial2 orelse not strict then
     make_target ((serial1, serializer),
-      ((merge (op =) (reserved1, reserved2), Symtab.merge (op =) (includes1, includes2)),
+      ((merge (op =) (reserved1, reserved2), Symtab.merge (K true) (includes1, includes2)),
         (merge_name_syntax_table (name_syntax_table1, name_syntax_table2),
-          Symtab.join (K snd) (module_alias1, module_alias2))
+          Symtab.join (K fst) (module_alias1, module_alias2))
     ))
   else
     error ("Incompatible serializers: " ^ quote target);
diff -r 456dd03e8cce -r f5a4b7ac635f src/Tools/induct.ML
--- a/src/Tools/induct.ML	Thu Jun 24 18:45:31 2010 +0200
+++ b/src/Tools/induct.ML	Thu Jun 24 21:03:32 2010 +0200
@@ -4,7 +4,7 @@
 Proof by cases, induction, and coinduction.
 *)
 
-signature INDUCT_DATA =
+signature INDUCT_ARGS =
 sig
   val cases_default: thm
   val atomize: thm list
@@ -82,27 +82,17 @@
   val setup: theory -> theory
 end;
 
-functor Induct(Data: INDUCT_DATA): INDUCT =
+functor Induct(Induct_Args: INDUCT_ARGS): INDUCT =
 struct
 
-
-(** misc utils **)
-
-(* encode_type -- for indexing purposes *)
-
-fun encode_type (Type (c, Ts)) = Term.list_comb (Const (c, dummyT), map encode_type Ts)
-  | encode_type (TFree (a, _)) = Free (a, dummyT)
-  | encode_type (TVar (a, _)) = Var (a, dummyT);
-
-
-(* variables -- ordered left-to-right, preferring right *)
+(** variables -- ordered left-to-right, preferring right **)
 
 fun vars_of tm =
   rev (distinct (op =) (Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm []));
 
 local
 
-val mk_var = encode_type o #2 o Term.dest_Var;
+val mk_var = Net.encode_type o #2 o Term.dest_Var;
 
 fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle Empty =>
   raise THM ("No variables in conclusion of rule", 0, [thm]);
@@ -128,14 +118,14 @@
     fun conv1 0 ctxt = Conv.forall_conv (cv o snd) ctxt
       | conv1 k ctxt =
           Conv.rewr_conv @{thm swap_params} then_conv
-          Conv.forall_conv (conv1 (k-1) o snd) ctxt
+          Conv.forall_conv (conv1 (k - 1) o snd) ctxt
     fun conv2 0 ctxt = conv1 j ctxt
-      | conv2 k ctxt = Conv.forall_conv (conv2 (k-1) o snd) ctxt
+      | conv2 k ctxt = Conv.forall_conv (conv2 (k - 1) o snd) ctxt
   in conv2 i ctxt end;
 
 fun swap_prems_conv 0 = Conv.all_conv
   | swap_prems_conv i =
-      Conv.implies_concl_conv (swap_prems_conv (i-1)) then_conv
+      Conv.implies_concl_conv (swap_prems_conv (i - 1)) then_conv
       Conv.rewr_conv Drule.swap_prems_eq
 
 fun drop_judgment ctxt = Object_Logic.drop_judgment (ProofContext.theory_of ctxt);
@@ -145,46 +135,51 @@
     val l = length (Logic.strip_params t);
     val Hs = Logic.strip_assums_hyp t;
     fun find (i, t) =
-      case Data.dest_def (drop_judgment ctxt t) of
+      (case Induct_Args.dest_def (drop_judgment ctxt t) of
         SOME (Bound j, _) => SOME (i, j)
       | SOME (_, Bound j) => SOME (i, j)
-      | _ => NONE
+      | _ => NONE);
   in
-    case get_first find (map_index I Hs) of
+    (case get_first find (map_index I Hs) of
       NONE => NONE
     | SOME (0, 0) => NONE
-    | SOME (i, j) => SOME (i, l-j-1, j)
+    | SOME (i, j) => SOME (i, l - j - 1, j))
   end;
 
-fun mk_swap_rrule ctxt ct = case find_eq ctxt (term_of ct) of
+fun mk_swap_rrule ctxt ct =
+  (case find_eq ctxt (term_of ct) of
     NONE => NONE
-  | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct);
+  | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct));
 
-val rearrange_eqs_simproc = Simplifier.simproc
-  (Thm.theory_of_thm Drule.swap_prems_eq) "rearrange_eqs" ["all t"]
-  (fn thy => fn ss => fn t =>
-     mk_swap_rrule (Simplifier.the_context ss) (cterm_of thy t))
+val rearrange_eqs_simproc =
+  Simplifier.simproc
+    (Thm.theory_of_thm Drule.swap_prems_eq) "rearrange_eqs" ["all t"]
+    (fn thy => fn ss => fn t =>
+      mk_swap_rrule (Simplifier.the_context ss) (cterm_of thy t));
+
 
 (* rotate k premises to the left by j, skipping over first j premises *)
 
 fun rotate_conv 0 j 0 = Conv.all_conv
-  | rotate_conv 0 j k = swap_prems_conv j then_conv rotate_conv 1 j (k-1)
-  | rotate_conv i j k = Conv.implies_concl_conv (rotate_conv (i-1) j k);
+  | rotate_conv 0 j k = swap_prems_conv j then_conv rotate_conv 1 j (k - 1)
+  | rotate_conv i j k = Conv.implies_concl_conv (rotate_conv (i - 1) j k);
 
 fun rotate_tac j 0 = K all_tac
-  | rotate_tac j k = SUBGOAL (fn (goal, i) => CONVERSION (rotate_conv
-      j (length (Logic.strip_assums_hyp goal) - j - k) k) i);
+  | rotate_tac j k = SUBGOAL (fn (goal, i) =>
+      CONVERSION (rotate_conv
+        j (length (Logic.strip_assums_hyp goal) - j - k) k) i);
+
 
 (* rulify operators around definition *)
 
 fun rulify_defs_conv ctxt ct =
-  if exists_subterm (is_some o Data.dest_def) (term_of ct) andalso
-    not (is_some (Data.dest_def (drop_judgment ctxt (term_of ct))))
+  if exists_subterm (is_some o Induct_Args.dest_def) (term_of ct) andalso
+    not (is_some (Induct_Args.dest_def (drop_judgment ctxt (term_of ct))))
   then
     (Conv.forall_conv (rulify_defs_conv o snd) ctxt else_conv
      Conv.implies_conv (Conv.try_conv (rulify_defs_conv ctxt))
        (Conv.try_conv (rulify_defs_conv ctxt)) else_conv
-     Conv.first_conv (map Conv.rewr_conv Data.rulify) then_conv
+     Conv.first_conv (map Conv.rewr_conv Induct_Args.rulify) then_conv
        Conv.try_conv (rulify_defs_conv ctxt)) ct
   else Conv.no_conv ct;
 
@@ -213,7 +208,7 @@
 
 (* context data *)
 
-structure InductData = Generic_Data
+structure Data = Generic_Data
 (
   type T = (rules * rules) * (rules * rules) * (rules * rules) * simpset;
   val empty =
@@ -230,7 +225,7 @@
      merge_ss (simpset1, simpset2));
 );
 
-val get_local = InductData.get o Context.Proof;
+val get_local = Data.get o Context.Proof;
 
 fun dest_rules ctxt =
   let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP), _) = get_local ctxt in
@@ -272,11 +267,11 @@
 fun find_rules which how ctxt x =
   map snd (Item_Net.retrieve (which (get_local ctxt)) (how x));
 
-val find_casesT = find_rules (#1 o #1) encode_type;
+val find_casesT = find_rules (#1 o #1) Net.encode_type;
 val find_casesP = find_rules (#2 o #1) I;
-val find_inductT = find_rules (#1 o #2) encode_type;
+val find_inductT = find_rules (#1 o #2) Net.encode_type;
 val find_inductP = find_rules (#2 o #2) I;
-val find_coinductT = find_rules (#1 o #3) encode_type;
+val find_coinductT = find_rules (#1 o #3) Net.encode_type;
 val find_coinductP = find_rules (#2 o #3) I;
 
 
@@ -286,10 +281,11 @@
 local
 
 fun mk_att f g name arg =
-  let val (x, thm) = g arg in (InductData.map (f (name, thm)) x, thm) end;
+  let val (x, thm) = g arg in (Data.map (f (name, thm)) x, thm) end;
 
-fun del_att which = Thm.declaration_attribute (fn th => InductData.map (which (pairself (fn rs =>
-  fold Item_Net.remove (filter_rules rs th) rs))));
+fun del_att which =
+  Thm.declaration_attribute (fn th => Data.map (which (pairself (fn rs =>
+    fold Item_Net.remove (filter_rules rs th) rs))));
 
 fun map1 f (x, y, z, s) = (f x, y, z, s);
 fun map2 f (x, y, z, s) = (x, f y, z, s);
@@ -320,12 +316,12 @@
 val coinduct_pred = mk_att add_coinductP consumes1;
 val coinduct_del = del_att map3;
 
-fun map_simpset f = InductData.map (map4 f);
+fun map_simpset f = Data.map (map4 f);
 
 fun induct_simp f =
   Thm.declaration_attribute (fn thm => fn context =>
-      (map_simpset
-        (Simplifier.with_context (Context.proof_of context) (fn ss => f (ss, [thm]))) context));
+      map_simpset
+        (Simplifier.with_context (Context.proof_of context) (fn ss => f (ss, [thm]))) context);
 
 val induct_simp_add = induct_simp (op addsimps);
 val induct_simp_del = induct_simp (op delsimps);
@@ -420,14 +416,15 @@
 
 (* mark equality constraints in cases rule *)
 
-val equal_def' = Thm.symmetric Data.equal_def;
+val equal_def' = Thm.symmetric Induct_Args.equal_def;
 
 fun mark_constraints n ctxt = Conv.fconv_rule
   (Conv.prems_conv (~1) (Conv.params_conv ~1 (K (Conv.prems_conv n
      (MetaSimplifier.rewrite false [equal_def']))) ctxt));
 
 val unmark_constraints = Conv.fconv_rule
-  (MetaSimplifier.rewrite true [Data.equal_def]);
+  (MetaSimplifier.rewrite true [Induct_Args.equal_def]);
+
 
 (* simplify *)
 
@@ -435,7 +432,7 @@
   Simplifier.full_rewrite (Simplifier.context ctxt (#4 (get_local ctxt)));
 
 fun simplify_conv ctxt ct =
-  if exists_subterm (is_some o Data.dest_def) (term_of ct) then
+  if exists_subterm (is_some o Induct_Args.dest_def) (term_of ct) then
     (Conv.try_conv (rulify_defs_conv ctxt) then_conv simplify_conv' ctxt) ct
   else Conv.all_conv ct;
 
@@ -447,7 +444,7 @@
 
 fun simplify_tac ctxt = CONVERSION (simplify_conv ctxt);
 
-val trivial_tac = Data.trivial_tac;
+val trivial_tac = Induct_Args.trivial_tac;
 
 
 
@@ -487,7 +484,7 @@
       (case opt_rule of
         SOME r => Seq.single (inst_rule r)
       | NONE =>
-          (get_casesP ctxt facts @ get_casesT ctxt insts @ [Data.cases_default])
+          (get_casesP ctxt facts @ get_casesT ctxt insts @ [Induct_Args.cases_default])
           |> tap (trace_rules ctxt casesN)
           |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
   in
@@ -517,12 +514,12 @@
 (* atomize *)
 
 fun atomize_term thy =
-  MetaSimplifier.rewrite_term thy Data.atomize []
+  MetaSimplifier.rewrite_term thy Induct_Args.atomize []
   #> Object_Logic.drop_judgment thy;
 
-val atomize_cterm = MetaSimplifier.rewrite true Data.atomize;
+val atomize_cterm = MetaSimplifier.rewrite true Induct_Args.atomize;
 
-val atomize_tac = Simplifier.rewrite_goal_tac Data.atomize;
+val atomize_tac = Simplifier.rewrite_goal_tac Induct_Args.atomize;
 
 val inner_atomize_tac =
   Simplifier.rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac;
@@ -531,8 +528,8 @@
 (* rulify *)
 
 fun rulify_term thy =
-  MetaSimplifier.rewrite_term thy (Data.rulify @ conjunction_congs) [] #>
-  MetaSimplifier.rewrite_term thy Data.rulify_fallback [];
+  MetaSimplifier.rewrite_term thy (Induct_Args.rulify @ conjunction_congs) [] #>
+  MetaSimplifier.rewrite_term thy Induct_Args.rulify_fallback [];
 
 fun rulified_term thm =
   let
@@ -542,8 +539,8 @@
   in (thy, Logic.list_implies (map rulify As, rulify B)) end;
 
 val rulify_tac =
-  Simplifier.rewrite_goal_tac (Data.rulify @ conjunction_congs) THEN'
-  Simplifier.rewrite_goal_tac Data.rulify_fallback THEN'
+  Simplifier.rewrite_goal_tac (Induct_Args.rulify @ conjunction_congs) THEN'
+  Simplifier.rewrite_goal_tac Induct_Args.rulify_fallback THEN'
   Goal.conjunction_tac THEN_ALL_NEW
   (Simplifier.rewrite_goal_tac [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac);