# HG changeset patch
# User blanchet
# Date 1381170854 -7200
# Node ID 5752a39e482e56c8dc9f50775238b3adca7698e6
# Parent  1a13325269c24a22859529aea7f84a1fdb6d863f
minor doc fix

diff -r 1a13325269c2 -r 5752a39e482e src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Oct 07 08:39:50 2013 -0700
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Oct 07 20:34:14 2013 +0200
@@ -1800,8 +1800,8 @@
 function translates a DFA into a @{type state_machine}:
 *}
 
-    primcorec (*<*)(in early) (*>*)
-      sm_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> 'a state_machine"
+    primcorec
+      (*<*)(in early) (*>*)sm_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> 'a state_machine"
     where
       "sm_of_dfa \<delta> F q = State_Machine (q \<in> F) (sm_of_dfa \<delta> F o \<delta> q)"