src/HOL/Statespace/state_space.ML
changeset 38389 d7d915bae307
parent 38350 480b2de9927c
child 38549 d0385f2764d8
     1.1 --- a/src/HOL/Statespace/state_space.ML	Thu Aug 12 13:23:46 2010 +0200
     1.2 +++ b/src/HOL/Statespace/state_space.ML	Thu Aug 12 13:28:18 2010 +0200
     1.3 @@ -466,7 +466,7 @@
     1.4                  (suffix valuetypesN full_name,(("",false),Expression.Named  []))],[]) fixestate
     1.5       |> ProofContext.theory_of 
     1.6       |> fold interprete_parent parents
     1.7 -     |> add_declaration (SOME full_name) (declare_declinfo components')
     1.8 +     |> add_declaration full_name (declare_declinfo components')
     1.9    end;
    1.10  
    1.11