# HG changeset patch
# User wenzelm
# Date 1393796374 -3600
# Node ID 1bfe72d146305ebb5dec607e415f6ea5a74b3441
# Parent  c38ad094e5bfd72f2dbcb16a68c0b87e5c432511
more standard module name;

diff -r c38ad094e5bf -r 1bfe72d14630 src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Sun Mar 02 22:37:55 2014 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Sun Mar 02 22:39:34 2014 +0100
@@ -325,7 +325,7 @@
 
 ML_file "langford.ML"
 method_setup dlo = {*
-  Scan.succeed (SIMPLE_METHOD' o LangfordQE.dlo_tac)
+  Scan.succeed (SIMPLE_METHOD' o Langford.dlo_tac)
 *} "Langford's algorithm for quantifier elimination in dense linear orders"
 
 
diff -r c38ad094e5bf -r 1bfe72d14630 src/HOL/Decision_Procs/langford.ML
--- a/src/HOL/Decision_Procs/langford.ML	Sun Mar 02 22:37:55 2014 +0100
+++ b/src/HOL/Decision_Procs/langford.ML	Sun Mar 02 22:39:34 2014 +0100
@@ -2,13 +2,13 @@
     Author:     Amine Chaieb, TU Muenchen
 *)
 
-signature LANGFORD_QE =
+signature LANGFORD =
 sig
   val dlo_tac : Proof.context -> int -> tactic
   val dlo_conv : Proof.context -> cterm -> thm
 end
 
-structure LangfordQE: LANGFORD_QE =
+structure Langford: LANGFORD =
 struct
 
 val dest_set =