--- a/src/Pure/ML/ml_antiquotations.ML Mon Apr 04 17:25:53 2016 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML Mon Apr 04 19:48:54 2016 +0200
@@ -10,12 +10,7 @@
(* ML support *)
val _ = Theory.setup
- (ML_Antiquotation.value @{binding cartouche}
- (Scan.lift Args.cartouche_input >> (fn source =>
- "Input.source true " ^ ML_Syntax.print_string (Input.text_of source) ^ " " ^
- ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source)))) #>
-
- ML_Antiquotation.inline @{binding undefined}
+ (ML_Antiquotation.inline @{binding undefined}
(Scan.succeed "(raise General.Match)") #>
ML_Antiquotation.inline @{binding assert}