Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Sun, 06 Nov 2011 17:05:45 +0100
changeset 45361 6fe8bf57319b
parent 45360 09bef4e1cc55
child 45362 dc605ed5a40d
tuned;
src/HOL/Statespace/state_fun.ML file | annotate | diff | comparison | revisions
src/HOL/Statespace/state_space.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Statespace/state_fun.ML	Sun Nov 06 17:00:05 2011 +0100
+++ b/src/HOL/Statespace/state_fun.ML	Sun Nov 06 17:05:45 2011 +0100
@@ -147,7 +147,7 @@
            then NONE
            else SOME thm
         end
-        handle Option => NONE)
+        handle Option.Option => NONE)
          
       | _ => NONE ));
 
@@ -312,7 +312,7 @@
              in SOME thm' end
              handle TERM _ => NONE)
           | _ => NONE)
-        end handle Option => NONE) 
+        end handle Option.Option => NONE) 
 end;
 
 val val_sfx = "V";
--- a/src/HOL/Statespace/state_space.ML	Sun Nov 06 17:00:05 2011 +0100
+++ b/src/HOL/Statespace/state_space.ML	Sun Nov 06 17:05:45 2011 +0100
@@ -213,7 +213,7 @@
     val y_path = the (DistinctTreeProver.find_tree y tree);
     val thm = DistinctTreeProver.distinctTreeProver dist_thm x_path y_path;
   in SOME thm
-  end handle Option => NONE)
+  end handle Option.Option => NONE)
 
 fun distinctTree_tac ctxt = SUBGOAL (fn (goal, i) =>
   (case goal of
isabelle