# HG changeset patch
# User wenzelm
# Date 1439718921 -7200
# Node ID bb75b61dba5db8d26b32a95a969f5838eb18d8d3
# Parent  7cf1ea00a0201d246b13bd1f87567317eac3d06c
tuned whitespace;

diff -r 7cf1ea00a020 -r bb75b61dba5d src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sun Aug 16 11:46:08 2015 +0200
+++ b/src/Provers/classical.ML	Sun Aug 16 11:55:21 2015 +0200
@@ -324,8 +324,8 @@
     in
       CS
        {safeIs = Item_Net.update th safeIs,
-        safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair,
-        safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair,
+        safe0_netpair = insert (nI, nE) (safe0_rls, []) safe0_netpair,
+        safep_netpair = insert (nI, nE) (safep_rls, []) safep_netpair,
         safeEs = safeEs,
         unsafeIs = unsafeIs,
         unsafeEs = unsafeEs,
@@ -333,7 +333,7 @@
         uwrappers = uwrappers,
         unsafe_netpair = unsafe_netpair,
         dup_netpair = dup_netpair,
-        extra_netpair = insert' (the_default 0 w) (nI,nE) ([th], []) extra_netpair}
+        extra_netpair = insert' (the_default 0 w) (nI, nE) ([th], []) extra_netpair}
     end;
 
 fun addSE w opt_context th
@@ -353,8 +353,8 @@
     in
       CS
        {safeEs = Item_Net.update th safeEs,
-        safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair,
-        safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair,
+        safe0_netpair = insert (nI, nE) ([], safe0_rls) safe0_netpair,
+        safep_netpair = insert (nI, nE) ([], safep_rls) safep_netpair,
         safeIs = safeIs,
         unsafeIs = unsafeIs,
         unsafeEs = unsafeEs,
@@ -362,7 +362,7 @@
         uwrappers = uwrappers,
         unsafe_netpair = unsafe_netpair,
         dup_netpair = dup_netpair,
-        extra_netpair = insert' (the_default 0 w) (nI,nE) ([], [th]) extra_netpair}
+        extra_netpair = insert' (the_default 0 w) (nI, nE) ([], [th]) extra_netpair}
     end;
 
 fun addSD w opt_context th = addSE w opt_context (make_elim opt_context th);