# HG changeset patch
# User haftmann
# Date 1747816206 -7200
# Node ID 9e35c1662aecc172163140d97ce1880c4fce31a1
# Parent  f7007ebfb556d530cd55780c2daf9b122452f1cf
clarifed name of structure

diff -r f7007ebfb556 -r 9e35c1662aec src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Tue May 20 20:05:50 2025 +0200
+++ b/src/Pure/raw_simplifier.ML	Wed May 21 10:30:06 2025 +0200
@@ -1575,5 +1575,5 @@
 
 end;
 
-structure Basic_Meta_Simplifier: BASIC_RAW_SIMPLIFIER = Raw_Simplifier;
-open Basic_Meta_Simplifier;
+structure Basic_Raw_Simplifier: BASIC_RAW_SIMPLIFIER = Raw_Simplifier;
+open Basic_Raw_Simplifier;