theorem names generated by the (rep_)datatype command now have mandatory qualifiers
authorhuffman
Fri Dec 03 10:03:13 2010 +0100 (2010-12-03)
changeset 409297ff03a5e044f
parent 40928 ace26e2cee91
child 40930 500171e7aa59
theorem names generated by the (rep_)datatype command now have mandatory qualifiers
src/HOL/Product_Type.thy
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/datatype_aux.ML
src/HOL/Tools/Datatype/datatype_data.ML
     1.1 --- a/src/HOL/Product_Type.thy	Fri Dec 03 10:03:10 2010 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Fri Dec 03 10:03:13 2010 +0100
     1.3 @@ -160,7 +160,7 @@
     1.4  
     1.5  declare prod.simps(2) [nitpick_simp del]
     1.6  
     1.7 -declare weak_case_cong [cong del]
     1.8 +declare prod.weak_case_cong [cong del]
     1.9  
    1.10  
    1.11  subsubsection {* Tuple syntax *}
    1.12 @@ -440,7 +440,7 @@
    1.13  
    1.14  lemma split_weak_cong: "p = q \<Longrightarrow> split c p = split c q"
    1.15    -- {* Prevents simplification of @{term c}: much faster *}
    1.16 -  by (fact weak_case_cong)
    1.17 +  by (fact prod.weak_case_cong)
    1.18  
    1.19  lemma cond_split_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g"
    1.20    by (simp add: split_eta)
    1.21 @@ -578,7 +578,7 @@
    1.22    \medskip @{term split} used as a logical connective or set former.
    1.23  
    1.24    \medskip These rules are for use with @{text blast}; could instead
    1.25 -  call @{text simp} using @{thm [source] split} as rewrite. *}
    1.26 +  call @{text simp} using @{thm [source] prod.split} as rewrite. *}
    1.27  
    1.28  lemma splitI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> split c p"
    1.29    apply (simp only: split_tupled_all)
     2.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Fri Dec 03 10:03:10 2010 +0100
     2.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Dec 03 10:03:13 2010 +0100
     2.3 @@ -628,9 +628,9 @@
     2.4  
     2.5      val ([dt_induct'], thy7) =
     2.6        thy6
     2.7 -      |> Sign.add_path big_name
     2.8 -      |> Global_Theory.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])]
     2.9 -      ||> Sign.parent_path
    2.10 +      |> Global_Theory.add_thms
    2.11 +        [((Binding.qualify true big_name (Binding.name "induct"), dt_induct),
    2.12 +          [case_names_induct])]
    2.13        ||> Theory.checkpoint;
    2.14  
    2.15    in
     3.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Dec 03 10:03:10 2010 +0100
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Dec 03 10:03:13 2010 +0100
     3.3 @@ -98,18 +98,18 @@
     3.4  
     3.5  fun store_thmss_atts label tnames attss thmss =
     3.6    fold_map (fn ((tname, atts), thms) =>
     3.7 -    Sign.add_path tname
     3.8 -    #> Global_Theory.add_thmss [((Binding.name label, thms), atts)]
     3.9 -    #-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss)
    3.10 +    Global_Theory.add_thmss
    3.11 +      [((Binding.qualify true tname (Binding.name label), thms), atts)]
    3.12 +    #-> (fn thm::_ => pair thm)) (tnames ~~ attss ~~ thmss)
    3.13    ##> Theory.checkpoint;
    3.14  
    3.15  fun store_thmss label tnames = store_thmss_atts label tnames (replicate (length tnames) []);
    3.16  
    3.17  fun store_thms_atts label tnames attss thmss =
    3.18    fold_map (fn ((tname, atts), thms) =>
    3.19 -    Sign.add_path tname
    3.20 -    #> Global_Theory.add_thms [((Binding.name label, thms), atts)]
    3.21 -    #-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss)
    3.22 +    Global_Theory.add_thms
    3.23 +      [((Binding.qualify true tname (Binding.name label), thms), atts)]
    3.24 +    #-> (fn thm::_ => pair thm)) (tnames ~~ attss ~~ thmss)
    3.25    ##> Theory.checkpoint;
    3.26  
    3.27  fun store_thms label tnames = store_thms_atts label tnames (replicate (length tnames) []);
     4.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Fri Dec 03 10:03:10 2010 +0100
     4.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Fri Dec 03 10:03:13 2010 +0100
     4.3 @@ -362,14 +362,14 @@
     4.4    let
     4.5      val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
     4.6      val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
     4.7 +    val prfx = Binding.qualify true (space_implode "_" new_type_names);
     4.8      val (((inject, distinct), [induct]), thy2) =
     4.9        thy1
    4.10        |> store_thmss "inject" new_type_names raw_inject
    4.11        ||>> store_thmss "distinct" new_type_names raw_distinct
    4.12 -      ||> Sign.add_path (space_implode "_" new_type_names)
    4.13        ||>> Global_Theory.add_thms
    4.14 -        [((Binding.name "induct", raw_induct), [mk_case_names_induct descr])]
    4.15 -      ||> Sign.restore_naming thy1;
    4.16 +        [((prfx (Binding.name "induct"), raw_induct),
    4.17 +          [mk_case_names_induct descr])];
    4.18    in
    4.19      thy2
    4.20      |> derive_datatype_props config dt_names alt_names [descr] sorts