src/Pure/ML/ml_antiquote.ML
changeset 41376 08240feb69c7
parent 40241 56fad09655a5
child 41486 82c1e348bc18
equal deleted inserted replaced
41375:7a89b4b94817 41376:08240feb69c7
    46 fun declaration kind name scan = ML_Context.add_antiq name
    46 fun declaration kind name scan = ML_Context.add_antiq name
    47   (fn _ => scan >> (fn s => fn background =>
    47   (fn _ => scan >> (fn s => fn background =>
    48     let
    48     let
    49       val (a, background') = variant (translate_string (fn "." => "_" | c => c) name) background;
    49       val (a, background') = variant (translate_string (fn "." => "_" | c => c) name) background;
    50       val env = kind ^ " " ^ a ^ " = " ^ s ^ ";\n";
    50       val env = kind ^ " " ^ a ^ " = " ^ s ^ ";\n";
    51       val body = "Isabelle." ^ a;
    51       val body = " Isabelle." ^ a ^ " ";
    52     in (K (env, body), background') end));
    52     in (K (env, body), background') end));
    53 
    53 
    54 val value = declaration "val";
    54 val value = declaration "val";
    55 
    55 
    56 
    56