src/Provers/classical.ML
changeset 9952 24914e42b857
parent 9941 fe05af7ec816
child 10034 4bca6b2d2589
     1.1 --- a/src/Provers/classical.ML	Wed Sep 13 22:29:37 2000 +0200
     1.2 +++ b/src/Provers/classical.ML	Wed Sep 13 22:31:19 2000 +0200
     1.3 @@ -1027,7 +1027,6 @@
     1.4  val elimN = "elim";
     1.5  val destN = "dest";
     1.6  val ruleN = "rule";
     1.7 -val delN = "del";
     1.8  
     1.9  val colon = Args.$$$ ":";
    1.10  val query = Args.$$$ "?";
    1.11 @@ -1040,7 +1039,7 @@
    1.12  
    1.13  fun cla_attr f g h = (cla_att change_global_cs f g h, cla_att change_local_cs f g h);
    1.14  
    1.15 -fun del_args att = Attrib.syntax (Scan.lift (Args.$$$ delN) >> K att);
    1.16 +fun del_args att = Attrib.syntax (Scan.lift (Args.$$$ Args.delN) >> K att);
    1.17  val rule_del_attr = (del_args rule_del_global, del_args rule_del_local);
    1.18  
    1.19  
    1.20 @@ -1159,7 +1158,7 @@
    1.21    Args.$$$ introN -- query_colon >> K (I, xtra_intro_local),
    1.22    Args.$$$ introN -- bang_colon >> K (I, safe_intro_local),
    1.23    Args.$$$ introN -- colon >> K (I, haz_intro_local),
    1.24 -  Args.$$$ delN -- colon >> K (I, rule_del_local)];
    1.25 +  Args.$$$ Args.delN -- colon >> K (I, rule_del_local)];
    1.26  
    1.27  fun cla_meth tac prems ctxt = Method.METHOD (fn facts =>
    1.28    ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_claset ctxt));