src/Pure/Isar/named_target.ML
changeset 45310 adaf2184b79d
parent 45298 aa35859c8741
child 45311 ca9e66c523a2
     1.1 --- a/src/Pure/Isar/named_target.ML	Sun Oct 30 09:42:13 2011 +0100
     1.2 +++ b/src/Pure/Isar/named_target.ML	Sun Oct 30 22:20:45 2011 +0100
     1.3 @@ -52,12 +52,12 @@
     1.4      val locale_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl;
     1.5    in
     1.6      lthy
     1.7 -    |> pervasive ? Generic_Target.theory_declaration syntax decl
     1.8 +    |> pervasive ? Generic_Target.theory_declaration decl
     1.9      |> Local_Theory.target (add locale locale_decl)
    1.10    end;
    1.11  
    1.12  fun target_declaration (Target {target, ...}) params =
    1.13 -  if target = "" then Generic_Target.theory_declaration (#syntax params)
    1.14 +  if target = "" then Generic_Target.theory_declaration
    1.15    else locale_declaration target params;
    1.16  
    1.17