src/Pure/Isar/proof_context.ML
changeset 6560 1436349f8b28
parent 6550 68f950b1a664
child 6721 dcee829f8e21
     1.1 --- a/src/Pure/Isar/proof_context.ML	Fri Apr 30 18:25:10 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Sat May 01 00:10:05 1999 +0200
     1.3 @@ -382,7 +382,7 @@
     1.4  
     1.5  (* dummy patterns *)
     1.6  
     1.7 -fun is_dummy (Const ("dummy", _)) = true
     1.8 +fun is_dummy (Const (c, _)) = c = PureThy.dummy_patternN
     1.9    | is_dummy _ = false;
    1.10  
    1.11  fun reject_dummies ctxt tm =
    1.12 @@ -390,8 +390,8 @@
    1.13    else raise CONTEXT ("Illegal dummy pattern(s) in term", ctxt);
    1.14  
    1.15  
    1.16 -fun prep_dummy (i, Const ("dummy", T)) = (i + 1, Var (("_dummy_", i), T))
    1.17 -  | prep_dummy i_t = i_t;
    1.18 +fun prep_dummy (i, t) =
    1.19 +  if is_dummy t then (i + 1, Var (("_dummy_", i), Term.fastype_of t)) else (i, t);
    1.20  
    1.21  fun prepare_dummies tm = #2 (Term.foldl_map_aterms prep_dummy (1, tm));
    1.22