src/HOL/Bali/WellType.thy
changeset 13462 56610e2ba220
parent 13384 a34e38154413
child 13524 604d0f3622d6
     1.1 --- a/src/HOL/Bali/WellType.thy	Tue Aug 06 11:20:47 2002 +0200
     1.2 +++ b/src/HOL/Bali/WellType.thy	Tue Aug 06 11:22:05 2002 +0200
     1.3 @@ -620,7 +620,7 @@
     1.4       _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
     1.5         x))) $ _ )) = is_Inj x
     1.6  in
     1.7 -  make_simproc name lhs pred (thm name)
     1.8 +  cond_simproc name lhs pred (thm name)
     1.9  end
    1.10  
    1.11  val wt_expr_proc  = wt_fun "wt_expr_eq"  "In1l" "\<exists>T.  U=Inl T  \<and> E,dt\<Turnstile>t\<Colon>-T"