# HG changeset patch # User wenzelm # Date 1265486227 -3600 # Node ID f3d49165889316df39adfdaec77f5a6e6752665d # Parent c3e3ac3ca0919ff4041a23a577eeb494deb986ff fixed spelling; diff -r c3e3ac3ca091 -r f3d491658893 src/Pure/Isar/args.ML --- a/src/Pure/Isar/args.ML Sat Feb 06 16:32:34 2010 +0100 +++ b/src/Pure/Isar/args.ML Sat Feb 06 20:57:07 2010 +0100 @@ -1,7 +1,7 @@ (* Title: Pure/Isar/args.ML Author: Markus Wenzel, TU Muenchen -Parsing with implicit value assigment. Concrete argument syntax of +Parsing with implicit value assignment. Concrete argument syntax of attributes, methods etc. *) diff -r c3e3ac3ca091 -r f3d491658893 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Sat Feb 06 16:32:34 2010 +0100 +++ b/src/Pure/System/session.scala Sat Feb 06 20:57:07 2010 +0100 @@ -122,14 +122,13 @@ // global status message result.body match { - // document state assigment + // document state assignment case List(XML.Elem(Markup.ASSIGN, _, edits)) if target_id.isDefined => documents.get(target_id.get) match { case Some(doc) => val states = for { - XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _) - <- edits + XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _) <- edits cmd <- lookup_command(cmd_id) } yield { val st = cmd.assign_state(state_id) diff -r c3e3ac3ca091 -r f3d491658893 src/Pure/type_infer.ML --- a/src/Pure/type_infer.ML Sat Feb 06 16:32:34 2010 +0100 +++ b/src/Pure/type_infer.ML Sat Feb 06 20:57:07 2010 +0100 @@ -284,7 +284,7 @@ | meets _ tye_idx = tye_idx; - (* occurs check and assigment *) + (* occurs check and assignment *) fun occurs_check tye i (Param (i', S)) = if i = i' then raise NO_UNIFIER ("Occurs check!", tye)