src/Pure/term.ML
changeset 56241 029246729dc0
parent 54732 b01bb3d09928
child 56243 2e10a36b8d46
     1.1 --- a/src/Pure/term.ML	Fri Mar 21 11:06:39 2014 +0100
     1.2 +++ b/src/Pure/term.ML	Fri Mar 21 11:42:32 2014 +0100
     1.3 @@ -924,18 +924,18 @@
     1.4  
     1.5  (* dummy patterns *)
     1.6  
     1.7 -fun dummy_pattern T = Const ("dummy_pattern", T);
     1.8 +fun dummy_pattern T = Const ("Pure.dummy_pattern", T);
     1.9  val dummy = dummy_pattern dummyT;
    1.10  val dummy_prop = dummy_pattern propT;
    1.11  
    1.12 -fun is_dummy_pattern (Const ("dummy_pattern", _)) = true
    1.13 +fun is_dummy_pattern (Const ("Pure.dummy_pattern", _)) = true
    1.14    | is_dummy_pattern _ = false;
    1.15  
    1.16  fun no_dummy_patterns tm =
    1.17    if not (fold_aterms (fn t => fn b => b orelse is_dummy_pattern t) tm false) then tm
    1.18    else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
    1.19  
    1.20 -fun free_dummy_patterns (Const ("dummy_pattern", T)) used =
    1.21 +fun free_dummy_patterns (Const ("Pure.dummy_pattern", T)) used =
    1.22        let val [x] = Name.invent used Name.uu 1
    1.23        in (Free (Name.internal x, T), Name.declare x used) end
    1.24    | free_dummy_patterns (Abs (x, T, b)) used =
    1.25 @@ -948,7 +948,7 @@
    1.26        in (t' $ u', used'') end
    1.27    | free_dummy_patterns a used = (a, used);
    1.28  
    1.29 -fun replace_dummy Ts (Const ("dummy_pattern", T)) i =
    1.30 +fun replace_dummy Ts (Const ("Pure.dummy_pattern", T)) i =
    1.31        (list_comb (Var (("_dummy_", i), Ts ---> T), map_range Bound (length Ts)), i + 1)
    1.32    | replace_dummy Ts (Abs (x, T, t)) i =
    1.33        let val (t', i') = replace_dummy (T :: Ts) t i