src/Pure/Isar/isar_cmd.ML
changeset 45291 57cd50f98fdc
parent 44338 700008399ee5
child 45488 6d71d9e52369
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Fri Oct 28 17:15:52 2011 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Fri Oct 28 22:17:30 2011 +0200
     1.3 @@ -202,9 +202,8 @@
     1.4    ML_Lex.read pos txt
     1.5    |> ML_Context.expression pos
     1.6      "val declaration: Morphism.declaration"
     1.7 -    ("Context.map_proof (Local_Theory." ^
     1.8 -      (if syntax then "syntax_declaration" else "declaration") ^ " " ^
     1.9 -      Bool.toString pervasive ^ " declaration)")
    1.10 +    ("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \
    1.11 +      \pervasive = " ^ Bool.toString pervasive ^ "} declaration)")
    1.12    |> Context.proof_map;
    1.13  
    1.14