src/HOL/Tools/function_package/fundef_package.ML
changeset 26529 03ad378ed5f0
parent 26171 5426a823455c
child 26580 c3e597a476fd
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Thu Apr 03 16:03:59 2008 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Apr 03 16:34:52 2008 +0200
     1.3 @@ -40,11 +40,12 @@
     1.4  
     1.5  fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" 
     1.6  
     1.7 -fun add_simps fnames post sort label moreatts simps lthy =
     1.8 +fun add_simps fnames post sort extra_qualify label moreatts simps lthy =
     1.9      let
    1.10        val atts = Attrib.internal (K Simplifier.simp_add) :: moreatts
    1.11        val spec = post simps
    1.12                     |> map (apfst (apsnd (append atts)))
    1.13 +                   |> map (apfst (apfst extra_qualify))
    1.14  
    1.15        val (saved_spec_simps, lthy) =
    1.16          fold_map note_theorem spec lthy
    1.17 @@ -61,7 +62,7 @@
    1.18  
    1.19  fun fundef_afterqed config fixes post defname cont sort_cont cnames [[proof]] lthy =
    1.20      let
    1.21 -      val FundefResult {fs, R, psimps, trsimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = 
    1.22 +      val FundefResult {fs, R, psimps, trsimps,  simple_pinducts, termination, domintros, cases, ...} = 
    1.23            cont (Goal.close_result proof)
    1.24  
    1.25        val fnames = map (fst o fst) fixes
    1.26 @@ -70,8 +71,8 @@
    1.27  
    1.28        val (((psimps', pinducts'), (_, [termination'])), lthy) =
    1.29            lthy
    1.30 -            |> addsmps "psimps" [] psimps
    1.31 -            ||> fold_option (snd oo addsmps "simps" []) trsimps
    1.32 +            |> addsmps (NameSpace.qualified "partial") "psimps" [] psimps
    1.33 +            ||> fold_option (snd oo addsmps I "simps" []) trsimps
    1.34              ||>> note_theorem ((qualify "pinduct",
    1.35                     [Attrib.internal (K (RuleCases.case_names cnames)),
    1.36                      Attrib.internal (K (RuleCases.consumes 1)),
    1.37 @@ -125,7 +126,7 @@
    1.38        val qualify = NameSpace.qualified defname;
    1.39      in
    1.40        lthy
    1.41 -        |> add_simps "simps" allatts tsimps |> snd
    1.42 +        |> add_simps I "simps" allatts tsimps |> snd
    1.43          |> note_theorem ((qualify "induct", [Attrib.internal (K (RuleCases.case_names case_names))]), tinduct) |> snd
    1.44      end
    1.45