# HG changeset patch
# User haftmann
# Date 1330709214 -3600
# Node ID 07f9eda810b3b716c5ae64dc1343a013796ca0b3
# Parent  a65e18ceb1e3d98cecefa747ad4bb4053eeda2da
tuned whitespace

diff -r a65e18ceb1e3 -r 07f9eda810b3 src/HOL/Library/Reflection.thy
--- a/src/HOL/Library/Reflection.thy	Fri Mar 02 15:18:05 2012 +0100
+++ b/src/HOL/Library/Reflection.thy	Fri Mar 02 18:26:54 2012 +0100
@@ -16,7 +16,7 @@
 method_setup reify = {*
   Attrib.thms --
     Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")")) >>
-  (fn (eqs, to) => fn ctxt => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
+  (fn (eqs, to) => fn ctxt => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ fst (Reify_Data.get ctxt)) to))
 *} "partial automatic reification"
 
 method_setup reflection = {*
@@ -31,11 +31,11 @@
   thms --
   Scan.optional (keyword rulesN |-- thms) [] --
   Scan.option (keyword onlyN |-- Args.term) >>
-  (fn ((eqs,ths),to) => fn ctxt =>
+  (fn ((eqs, ths), to) => fn ctxt =>
     let
-      val (ceqs,cths) = Reify_Data.get ctxt
-      val corr_thms = ths@cths
-      val raw_eqs = eqs@ceqs
+      val (ceqs, cths) = Reify_Data.get ctxt
+      val corr_thms = ths @ cths
+      val raw_eqs = eqs @ ceqs
     in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) end)
 end
 *}