src/HOL/Tools/function_package/fundef_package.ML
changeset 21511 16c62deb1adf
parent 21491 574e63799847
child 21602 cb13024d0e36
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Fri Nov 24 13:39:22 2006 +0100
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Fri Nov 24 13:43:44 2006 +0100
     1.3 @@ -142,15 +142,15 @@
     1.4        val tsimps = PROFILE "making tsimps" (map remove_domain_condition) psimps
     1.5        val tinduct = PROFILE "making tinduct" (map remove_domain_condition) pinducts
     1.6  
     1.7 -        (* FIXME: How to generate code from (possibly) local contexts
     1.8 -        val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
     1.9 -        val allatts = if has_guards then [] else [Attrib.internal (RecfunCodegen.add NONE)]
    1.10 -        *)
    1.11 -        val qualify = NameSpace.qualified defname;
    1.12 +        (* FIXME: How to generate code from (possibly) local contexts*)
    1.13 +      val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
    1.14 +      val allatts = if has_guards then [] else [Attrib.internal (RecfunCodegen.add NONE)]
    1.15 +        
    1.16 +      val qualify = NameSpace.qualified defname;
    1.17      in
    1.18 -        lthy
    1.19 -          |> PROFILE "adding tsimps" (add_simps "simps" [] mutual fixes tsimps spec) |> snd
    1.20 -          |> PROFILE "adding tinduct" (note_theorem ((qualify "induct", []), tinduct)) |> snd
    1.21 +      lthy
    1.22 +        |> PROFILE "adding tsimps" (add_simps "simps" allatts mutual fixes tsimps spec) |> snd
    1.23 +        |> PROFILE "adding tinduct" (note_theorem ((qualify "induct", []), tinduct)) |> snd
    1.24      end
    1.25  
    1.26