# HG changeset patch
# User blanchet
# Date 1400500438 -7200
# Node ID 61855ade6c7e55694b7569ec01584a0585835376
# Parent  8d5e5ec1cac3ab4f697e632f9df2fbacbb0e2027
hide more consts to beautify documentation

diff -r 8d5e5ec1cac3 -r 61855ade6c7e src/Doc/Datatypes/Datatypes.thy
--- 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
 (*>*)
diff -r 8d5e5ec1cac3 -r 61855ade6c7e src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- 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