1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Mar 27 16:59:13 2012 +0300
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Mar 27 16:59:13 2012 +0300
     1.3 @@ -112,7 +112,14 @@
     1.4  val theory_const_suffix = Long_Name.separator ^ " 1"
     1.5  
     1.6  (* unfolding these can yield really huge terms *)
     1.7 -val risky_spec_eqs = @{thms Bit0_def Bit1_def}
     1.8 +val risky_defs = @{thms Bit0_def Bit1_def}
     1.9 +
    1.10 +fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))
    1.11 +fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t
    1.12 +  | is_rec_def (@{const ==>} $ _ $ t2) = is_rec_def t2
    1.13 +  | is_rec_def (Const (@{const_name "=="}, _) $ t1 $ t2) = is_rec_eq t1 t2
    1.14 +  | is_rec_def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2
    1.15 +  | is_rec_def _ = false
    1.16  
    1.17  fun clasimpset_rule_table_of ctxt =
    1.18    let
    1.19 @@ -138,22 +145,24 @@
    1.20  *)
    1.21      val simps = ctxt |> simpset_of |> dest_ss |> #simps
    1.22      val specs = ctxt |> Spec_Rules.get
    1.23 -    val spec_eqs =
    1.24 +    val (rec_defs, nonrec_defs) =
    1.25        specs |> filter (curry (op =) Spec_Rules.Equational o fst)
    1.26              |> maps (snd o snd)
    1.27 -            |> filter_out (member Thm.eq_thm_prop risky_spec_eqs)
    1.28 +            |> filter_out (member Thm.eq_thm_prop risky_defs)
    1.29 +            |> List.partition (is_rec_def o prop_of)
    1.30      val spec_intros =
    1.31        specs |> filter (member (op =) [Spec_Rules.Inductive,
    1.32                                        Spec_Rules.Co_Inductive] o fst)
    1.33              |> maps (snd o snd)
    1.34    in
    1.35      Termtab.empty |> add Simp [atomize] snd simps
    1.36 -                  |> add Spec_Eq [] I spec_eqs
    1.37 +                  |> add Simp [] I rec_defs
    1.38 +                  |> add Def [] I nonrec_defs
    1.39  (* Add once it is used:
    1.40                    |> add Elim [] I elims
    1.41  *)
    1.42                    |> add Intro [] I intros
    1.43 -                  |> add Spec_Intro [] I spec_intros
    1.44 +                  |> add Inductive [] I spec_intros
    1.45    end
    1.46  
    1.47  fun needs_quoting reserved s =
    1.48 @@ -184,7 +193,7 @@
    1.49    (* FIXME: use structured name *)
    1.50    if String.isSubstring ".induct" name orelse
    1.51       String.isSubstring ".inducts" name then
    1.52 -    Induct
    1.53 +    Induction
    1.54    else case Termtab.lookup css_table (prop_of th) of
    1.55      SOME status => status
    1.56    | NONE => General