--- a/src/Doc/Datatypes/Datatypes.thy Mon May 19 13:44:13 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Mon May 19 13:53:58 2014 +0200
@@ -194,7 +194,7 @@
*}
(*<*)
- hide_const None Some
+ hide_const None Some map_option
hide_type option
(*>*)
datatype_new 'a option = None | Some 'a
@@ -367,7 +367,7 @@
Cons (infixr "#" 65)
hide_type list
- hide_const Nil Cons hd tl set map list_all2
+ hide_const Nil Cons hd tl set map list_all2 rec_list size_list
context early begin
(*>*)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon May 19 13:44:13 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon May 19 13:53:58 2014 +0200
@@ -991,6 +991,7 @@
fun fact_has_right_theory (_, th) =
thy_name = Context.theory_name (theory_of_thm th)
+
fun chained_or_extra_features_of factor (((_, stature), th), weight) =
[prop_of th]
|> features_of ctxt (theory_of_thm th) num_facts const_tab stature false